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  2650  r3al  2672  r19.23t  2729  ceqsralt  2883  ralrab  2999  ralrab2  3003  euind  3024  reu2  3025  reu3  3027  rmo4  3030  reuind  3040  2reu5lem3  3044  rmo2  3132  rmo3  3134  ralss  3333  rabss  3344  unissb  3922  elintrab  3939  ssintrab  3950  peano5  4410  ssfin  4471  raliunxp  4824  fununi  5161  dff13  5472  clos1induct  5881  frds  5936  weds  5939  spacind  6288