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  692  pm4.14dc  890  pm5.6dc  926  2sb6  1984  2sb6rf  1990  2exsb  2009  mor  2068  eu2  2070  moanim  2100  r2alf  2494  r3al  2521  r19.23t  2584  ceqsralt  2765  rspc2gv  2854  ralrab  2899  ralrab2  2903  euind  2925  reu2  2926  reu3  2928  rmo4  2931  rmo3f  2935  reuind  2943  rmo2ilem  3053  rmo3  3055  ralss  3222  rabss  3233  raldifb  3276  unissb  3840  elintrab  3857  ssintrab  3868  dftr5  4105  repizf2lem  4162  reusv3  4461  tfi  4582  raliunxp  4769  fununi  5285  dff13  5769  dfsmo2  6288  tfr1onlemaccex  6349  tfrcllemaccex  6362  qliftfun  6617  nnnninfeq2  7127  prime  9352  raluz  9578  raluz2  9579  ralrp  9675  facwordi  10720  modfsummod  11466  nnwosdc  12040  isprm2  12117  isprm4  12119  metcnp  14015  limcdifap  14134  bdcriota  14638