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  2827  rspc2gv  2919  ralrab  2964  ralrab2  2968  euind  2990  reu2  2991  reu3  2993  rmo4  2996  rmo3f  3000  reuind  3008  rmo2ilem  3119  rmo3  3121  ralss  3290  rabss  3301  raldifb  3344  unissb  3917  elintrab  3934  ssintrab  3945  dftr5  4184  repizf2lem  4244  reusv3  4550  tfi  4673  raliunxp  4862  fununi  5388  dff13  5891  dfsmo2  6431  tfr1onlemaccex  6492  tfrcllemaccex  6505  qliftfun  6762  nnnninfeq2  7292  prime  9542  raluz  9769  raluz2  9770  ralrp  9867  facwordi  10957  modfsummod  11964  nnwosdc  12555  isprm2  12634  isprm4  12636  metcnp  15180  limcdifap  15330  bdcriota  16204  nnnninfex  16347