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

Theorem impexp 433
Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
Assertion
Ref Expression
impexp (((φ ψ) → χ) ↔ (φ → (ψχ)))

Proof of Theorem impexp
StepHypRef Expression
1 pm3.3 431 . 2 (((φ ψ) → χ) → (φ → (ψχ)))
2 pm3.31 432 . 2 ((φ → (ψχ)) → ((φ ψ) → χ))
31, 2impbii 180 1 (((φ ψ) → χ) ↔ (φ → (ψχ)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   wa 358
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
This theorem is referenced by:  pm4.14  561  nan  563  pm4.87  567  imp4a  572  exp4a  589  imdistan  670  pm5.3  692  pm5.6  878  exp3acom23g  1371  ax12bOLD  1690  2sb6  2113  2sb6rf  2118  2exsb  2132  eu2  2229  moanim  2260  2eu6  2289  r2alf  2649  r3al  2671  r19.23t  2728  ceqsralt  2882  ralrab  2998  ralrab2  3002  euind  3023  reu2  3024  reu3  3026  rmo4  3029  reuind  3039  2reu5lem3  3043  rmo2  3131  rmo3  3133  ralss  3332  rabss  3343  unissb  3921  elintrab  3938  ssintrab  3949  peano5  4409  ssfin  4470  raliunxp  4823  fununi  5160  dff13  5471  clos1induct  5880  frds  5935  weds  5938  spacind  6285
  Copyright terms: Public domain W3C validator