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  4234  repizf2lem  4300  reusv3  4608  tfi  4731  raliunxp  4923  fununi  5452  dff13  5977  dfsmo2  6563  tfr1onlemaccex  6624  tfrcllemaccex  6637  qliftfun  6896  nnnninfeq2  7475  prime  9755  raluz  9993  raluz2  9994  ralrp  10092  facwordi  11199  modfsummod  12249  nnwosdc  12840  isprm2  12919  isprm4  12921  metcnp  15755  limcdifap  15905  bdcriota  17131  nnnninfex  17288  dfrals2  17354  dfralseu2  17388