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  694  pm4.14dc  892  pm5.6dc  928  2sb6  2013  2sb6rf  2019  2exsb  2038  mor  2098  eu2  2100  moanim  2130  r2alf  2525  r3al  2552  r19.23t  2615  ceqsralt  2804  rspc2gv  2896  ralrab  2941  ralrab2  2945  euind  2967  reu2  2968  reu3  2970  rmo4  2973  rmo3f  2977  reuind  2985  rmo2ilem  3096  rmo3  3098  ralss  3267  rabss  3278  raldifb  3321  unissb  3894  elintrab  3911  ssintrab  3922  dftr5  4161  repizf2lem  4221  reusv3  4525  tfi  4648  raliunxp  4837  fununi  5361  dff13  5860  dfsmo2  6396  tfr1onlemaccex  6457  tfrcllemaccex  6470  qliftfun  6727  nnnninfeq2  7257  prime  9507  raluz  9734  raluz2  9735  ralrp  9832  facwordi  10922  modfsummod  11884  nnwosdc  12475  isprm2  12554  isprm4  12556  metcnp  15099  limcdifap  15249  bdcriota  16018  nnnninfex  16161