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

Theorem 3impia 1148
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impia.1
Assertion
Ref Expression
3impia

Proof of Theorem 3impia
StepHypRef Expression
1 3impia.1 . . 3
21ex 423 . 2
323imp 1145 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:  mopick2  2271  3gencl  2889  mob2  3016  moi  3019  reupick3  3540  disjne  3596  tfindi  4496  sfin112  4529  sfinltfin  4535  vfintle  4546  fvun1  5379  ovmpt4g  5710  ov2gf  5711  letc  6231  nclenn  6249  nchoicelem9  6297  nchoicelem17  6305  frecxp  6314
  Copyright terms: Public domain W3C validator