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  694  pm4.14dc  892  pm5.6dc  928  2sb6  2012  2sb6rf  2018  2exsb  2037  mor  2096  eu2  2098  moanim  2128  r2alf  2523  r3al  2550  r19.23t  2613  ceqsralt  2799  rspc2gv  2889  ralrab  2934  ralrab2  2938  euind  2960  reu2  2961  reu3  2963  rmo4  2966  rmo3f  2970  reuind  2978  rmo2ilem  3088  rmo3  3090  ralss  3259  rabss  3270  raldifb  3313  unissb  3880  elintrab  3897  ssintrab  3908  dftr5  4145  repizf2lem  4205  reusv3  4507  tfi  4630  raliunxp  4819  fununi  5342  dff13  5837  dfsmo2  6373  tfr1onlemaccex  6434  tfrcllemaccex  6447  qliftfun  6704  nnnninfeq2  7231  prime  9472  raluz  9699  raluz2  9700  ralrp  9797  facwordi  10885  modfsummod  11769  nnwosdc  12360  isprm2  12439  isprm4  12441  metcnp  14984  limcdifap  15134  bdcriota  15819  nnnninfex  15959