Theorem impexp 263

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 261	. 2 |- ( ( ( ph /\ ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )
2		pm3.31 262	. 2 |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph /\ ps ) -> ch ) )
3	1, 2	impbii 126	1 |- ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imp4a  349  exp4a  366  imdistan  444  pm5.3  475  pm4.87  557  nan  696  pm4.14dc  895  pm5.6dc  931  2sb6  2035  2sb6rf  2041  2exsb  2060  mor  2120  eu2  2122  moanim  2152  r2alf  2547  r3al  2574  r19.23t  2638  ceqsralt  2828  rspc2gv  2920  ralrab  2965  ralrab2  2969  euind  2991  reu2  2992  reu3  2994  rmo4  2997  rmo3f  3001  reuind  3009  rmo2ilem  3120  rmo3  3122  ralss  3291  rabss  3302  raldifb  3345  unissb  3921  elintrab  3938  ssintrab  3949  dftr5  4188  repizf2lem  4249  reusv3  4555  tfi  4678  raliunxp  4869  fununi  5395  dff13  5904  dfsmo2  6448  tfr1onlemaccex  6509  tfrcllemaccex  6522  qliftfun  6781  nnnninfeq2  7319  prime  9569  raluz  9802  raluz2  9803  ralrp  9900  facwordi  10992  modfsummod  12009  nnwosdc  12600  isprm2  12679  isprm4  12681  metcnp  15226  limcdifap  15376  bdcriota  16414  nnnninfex  16560