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

Theorem 3exp 1102
Description: Exportation inference. (Contributed by NM, 30-May-1994.)
Hypothesis
Ref Expression
3exp.1 ((φ ψ χ) → θ)
Assertion
Ref Expression
3exp (φ → (ψ → (χθ)))

Proof of Theorem 3exp
StepHypRef Expression
1 pm3.2an3 1082 . 2 (φ → (ψ → (χ → (φ ψ χ))))
2 3exp.1 . 2 ((φ ψ χ) → θ)
31, 2syl8 65 1 (φ → (ψ → (χθ)))
Colors of variables: wff set class
Syntax hints:  wi 4   w3a 884
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 886
This theorem is referenced by:  3expa  1103  3expb  1104  3expia  1105  3expib  1106  3com23  1109  3an1rs  1115  3exp1  1119  3expd  1120  exp5o  1122  syl3an2  1168  syl3an3  1169  3impexpbicomi  1325  rexlimdv3a  2429  rabssdv  3014  reupick2  3217  ssorduni  4179  tfisi  4253  fvssunirng  5133  f1oiso2  5409  poxp  5794  tfrlem5  5871  nndi  6004  nnmass  6005  mulcanpig  6319  divgt0  7599  divge0  7600  uzind  8105  uzind2  8106
  Copyright terms: Public domain W3C validator