ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3expia Structured version   GIF version

Theorem 3expia 1092
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1 ((φ ψ χ) → θ)
Assertion
Ref Expression
3expia ((φ ψ) → (χθ))

Proof of Theorem 3expia
StepHypRef Expression
1 3exp.1 . . 3 ((φ ψ χ) → θ)
213exp 1089 . 2 (φ → (ψ → (χθ)))
32imp 115 1 ((φ ψ) → (χθ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 873
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 875
This theorem is referenced by:  mp3an3  1206  3gencl  2565  moi  2701  sotricim  4034  suctr  4108  elirr  4208  en2lp  4216  suc11g  4219  3optocl  4345  sefvex  5121  f1oresrab  5254  ovmpt2s  5547  ov2gf  5548  poxp  5775  brtposg  5791  dfsmo2  5824  smoiun  5838  tfrlemibxssdm  5862  nnsucsssuc  5986  nnaordi  5992  nnawordex  6012  ltbtwnnqq  6272  prarloclem4  6352  addlocpr  6391  1idprl  6429  1idpru  6430  ltexprlemrnd  6442  recexprlemrnd  6463  recexprlem1ssl  6467  recexprlem1ssu  6468  recexprlemss1l  6469  recexprlemss1u  6470  ltxrlt  6686  bj-peano4  7177
  Copyright terms: Public domain W3C validator