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  559  nan  699  pm4.14dc  898  pm5.6dc  934  2sb6  2040  2sb6rf  2046  2exsb  2065  mor  2125  eu2  2127  moanim  2157  r2alf  2561  r3al  2588  r19.23t  2652  ceqsralt  2843  rspc2gv  2935  ralrab  2980  ralrab2  2984  euind  3006  reu2  3007  reu3  3009  rmo4  3012  rmo3f  3016  reuind  3024  rmo2ilem  3135  rmo3  3137  ralss  3306  rabss  3317  raldifb  3361  unissb  3946  elintrab  3963  ssintrab  3974  dftr5  4213  repizf2lem  4276  reusv3  4583  tfi  4706  raliunxp  4898  fununi  5426  dff13  5943  dfsmo2  6520  tfr1onlemaccex  6581  tfrcllemaccex  6594  qliftfun  6853  nnnninfeq2  7422  prime  9680  raluz  9913  raluz2  9914  ralrp  10011  facwordi  11106  modfsummod  12148  nnwosdc  12739  isprm2  12818  isprm4  12820  metcnp  15394  limcdifap  15544  bdcriota  16670  nnnninfex  16817