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  693  pm4.14dc  891  pm5.6dc  927  2sb6  2000  2sb6rf  2006  2exsb  2025  mor  2084  eu2  2086  moanim  2116  r2alf  2511  r3al  2538  r19.23t  2601  ceqsralt  2787  rspc2gv  2877  ralrab  2922  ralrab2  2926  euind  2948  reu2  2949  reu3  2951  rmo4  2954  rmo3f  2958  reuind  2966  rmo2ilem  3076  rmo3  3078  ralss  3246  rabss  3257  raldifb  3300  unissb  3866  elintrab  3883  ssintrab  3894  dftr5  4131  repizf2lem  4191  reusv3  4492  tfi  4615  raliunxp  4804  fununi  5323  dff13  5812  dfsmo2  6342  tfr1onlemaccex  6403  tfrcllemaccex  6416  qliftfun  6673  nnnninfeq2  7190  prime  9419  raluz  9646  raluz2  9647  ralrp  9744  facwordi  10814  modfsummod  11604  nnwosdc  12179  isprm2  12258  isprm4  12260  metcnp  14691  limcdifap  14841  bdcriota  15445