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

Theorem 3impa 1146
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impa.1
Assertion
Ref Expression
3impa

Proof of Theorem 3impa
StepHypRef Expression
1 3impa.1 . . 3
21exp31 587 . 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:  3impdir  1238  syl3an9b  1250  biimp3a  1281  rspec3  2714  rspc3v  2964  raltpg  3777  rextpg  3778  eladdci  4399  lefinlteq  4463  opelopabt  4699  3optocl  4840  fun2ssres  5145  funssfv  5343  foco2  5426  f1elima  5474  eloprabga  5578  mucass  6135  cenc  6181
  Copyright terms: Public domain W3C validator