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

Theorem 3imp 1145
 Description: Importation inference. (Contributed by NM, 8-Apr-1994.)
Hypothesis
Ref Expression
3imp.1 (φ → (ψ → (χθ)))
Assertion
Ref Expression
3imp ((φ ψ χ) → θ)

Proof of Theorem 3imp
StepHypRef Expression
1 df-3an 936 . 2 ((φ ψ χ) ↔ ((φ ψ) χ))
2 3imp.1 . . 3 (φ → (ψ → (χθ)))
32imp31 421 . 2 (((φ ψ) χ) → θ)
41, 3sylbi 187 1 ((φ ψ χ) → θ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∧ 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:  3impa  1146  3impb  1147  3impia  1148  3impib  1149  3com23  1157  3an1rs  1163  3imp1  1164  3impd  1165  syl3an2  1216  syl3an3  1217  3jao  1243  biimp3ar  1282  ltfintri  4466  ssfin  4470  nnadjoin  4520  sfintfin  4532  tfinnn  4534  nclenn  6249
 Copyright terms: Public domain W3C validator