NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  3exp GIF version

Theorem 3exp 1150
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 1131 . 2 (φ → (ψ → (χ → (φ ψ χ))))
2 3exp.1 . 2 ((φ ψ χ) → θ)
31, 2syl8 65 1 (φ → (ψ → (χθ)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   w3a 934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
This theorem is referenced by:  3expa  1151  3expb  1152  3expia  1153  3expib  1154  3com23  1157  3an1rs  1163  3exp1  1167  3expd  1168  exp5o  1170  syl3an2  1216  syl3an3  1217  3ecase  1286  3impexpbicomi  1368  rexlimdv3a  2740  rabssdv  3346  reupick2  3541  ssfin  4470  tfin11  4493  f1oiso2  5500  funsi  5520  trrd  5925  nchoicelem17  6305
  Copyright terms: Public domain W3C validator