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	|- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))

Proof of Theorem impexp

Step	Hyp	Ref	Expression
1		pm3.3 431	. 2 |- (((ph /\ ps) -> ch) -> (ph -> (ps -> ch)))
2		pm3.31 432	. 2 |- ((ph -> (ps -> ch)) -> ((ph /\ ps) -> ch))
3	1, 2	impbii 180	1 |- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358

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

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  6287