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  6562  tfr1onlemaccex  6623  tfrcllemaccex  6636  qliftfun  6895  nnnninfeq2  7475  prime  9756  raluz  9994  raluz2  9995  ralrp  10093  facwordi  11200  modfsummod  12250  nnwosdc  12841  isprm2  12920  isprm4  12922  metcnp  15738  limcdifap  15888  bdcriota  17114  nnnninfex  17271  dfrals2  17337  dfralseu2  17371