NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  3imp Unicode 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-1 5  ax-2 6  ax-3 7  ax-mp 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