Theorem impexp 260

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 258	. 2 |- ( ( ( ph /\ ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )
2		pm3.31 259	. 2 |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph /\ ps ) -> ch ) )
3	1, 2	impbii 125	1 |- ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imp4a  342  exp4a  359  imdistan  434  pm5.3  460  pm4.87  525  nan  662  pm4.14dc  826  pm5.6dc  874  2sb6  1909  2sb6rf  1915  2exsb  1934  mor  1991  eu2  1993  moanim  2023  r2alf  2396  r3al  2421  r19.23t  2480  ceqsralt  2647  rspc2gv  2734  ralrab  2777  ralrab2  2781  euind  2803  reu2  2804  reu3  2806  rmo4  2809  rmo3f  2813  reuind  2821  rmo2ilem  2929  rmo3  2931  ralss  3088  rabss  3099  raldifb  3141  unissb  3689  elintrab  3706  ssintrab  3717  dftr5  3945  repizf2lem  4002  reusv3  4295  tfi  4410  raliunxp  4590  fununi  5095  dff13  5561  dfsmo2  6066  tfr1onlemaccex  6127  tfrcllemaccex  6140  qliftfun  6388  prime  8899  raluz  9120  raluz2  9121  ralrp  9209  facwordi  10202  modfsummod  10906  isprm2  11431  isprm4  11433  bdcriota  12040