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  2011  2sb6rf  2017  2exsb  2036  mor  2095  eu2  2097  moanim  2127  r2alf  2522  r3al  2549  r19.23t  2612  ceqsralt  2798  rspc2gv  2888  ralrab  2933  ralrab2  2937  euind  2959  reu2  2960  reu3  2962  rmo4  2965  rmo3f  2969  reuind  2977  rmo2ilem  3087  rmo3  3089  ralss  3258  rabss  3269  raldifb  3312  unissb  3879  elintrab  3896  ssintrab  3907  dftr5  4144  repizf2lem  4204  reusv3  4506  tfi  4629  raliunxp  4818  fununi  5341  dff13  5836  dfsmo2  6372  tfr1onlemaccex  6433  tfrcllemaccex  6446  qliftfun  6703  nnnninfeq2  7230  prime  9471  raluz  9698  raluz2  9699  ralrp  9796  facwordi  10883  modfsummod  11740  nnwosdc  12331  isprm2  12410  isprm4  12412  metcnp  14955  limcdifap  15105  bdcriota  15781  nnnninfex  15921