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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imp4a  349  exp4a  366  imdistan  448  pm5.3  479  pm4.87  563  nan  703  pm4.14dc  902  pm5.6dc  938  2sb6  2044  2sb6rf  2050  2exsb  2069  mor  2129  eu2  2131  moanim  2161  r2alf  2567  r3al  2594  r19.23t  2658  ceqsralt  2849  rspc2gv  2942  ralrab  2987  ralrab2  2991  euind  3013  reu2  3014  reu3  3016  rmo4  3019  rmo3f  3023  reuind  3031  rmo2ilem  3142  rmo3  3144  ralss  3314  rabss  3325  raldifb  3369  unissb  3965  elintrab  3982  ssintrab  3993  dftr5  4232  repizf2lem  4298  reusv3  4606  tfi  4729  raliunxp  4921  fununi  5449  dff13  5974  dfsmo2  6558  tfr1onlemaccex  6619  tfrcllemaccex  6632  qliftfun  6891  nnnninfeq2  7469  prime  9745  raluz  9978  raluz2  9979  ralrp  10076  facwordi  11178  modfsummod  12225  nnwosdc  12816  isprm2  12895  isprm4  12897  metcnp  15613  limcdifap  15763  bdcriota  16909  nnnninfex  17065  dfrals2  17130  dfralseu2  17164