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  2764  rspc2gv  2853  ralrab  2898  ralrab2  2902  euind  2924  reu2  2925  reu3  2927  rmo4  2930  rmo3f  2934  reuind  2942  rmo2ilem  3052  rmo3  3054  ralss  3221  rabss  3232  raldifb  3275  unissb  3839  elintrab  3856  ssintrab  3867  dftr5  4104  repizf2lem  4161  reusv3  4460  tfi  4581  raliunxp  4768  fununi  5284  dff13  5768  dfsmo2  6287  tfr1onlemaccex  6348  tfrcllemaccex  6361  qliftfun  6616  nnnninfeq2  7126  prime  9350  raluz  9576  raluz2  9577  ralrp  9673  facwordi  10715  modfsummod  11461  nnwosdc  12034  isprm2  12111  isprm4  12113  metcnp  13905  limcdifap  14024  bdcriota  14517