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  2876  ralrab  2921  ralrab2  2925  euind  2947  reu2  2948  reu3  2950  rmo4  2953  rmo3f  2957  reuind  2965  rmo2ilem  3075  rmo3  3077  ralss  3245  rabss  3256  raldifb  3299  unissb  3865  elintrab  3882  ssintrab  3893  dftr5  4130  repizf2lem  4190  reusv3  4491  tfi  4614  raliunxp  4803  fununi  5322  dff13  5811  dfsmo2  6340  tfr1onlemaccex  6401  tfrcllemaccex  6414  qliftfun  6671  nnnninfeq2  7188  prime  9416  raluz  9643  raluz2  9644  ralrp  9741  facwordi  10811  modfsummod  11601  nnwosdc  12176  isprm2  12255  isprm4  12257  metcnp  14680  limcdifap  14816  bdcriota  15375