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  2097  eu2  2099  moanim  2129  r2alf  2524  r3al  2551  r19.23t  2614  ceqsralt  2801  rspc2gv  2893  ralrab  2938  ralrab2  2942  euind  2964  reu2  2965  reu3  2967  rmo4  2970  rmo3f  2974  reuind  2982  rmo2ilem  3092  rmo3  3094  ralss  3263  rabss  3274  raldifb  3317  unissb  3886  elintrab  3903  ssintrab  3914  dftr5  4153  repizf2lem  4213  reusv3  4515  tfi  4638  raliunxp  4827  fununi  5351  dff13  5850  dfsmo2  6386  tfr1onlemaccex  6447  tfrcllemaccex  6460  qliftfun  6717  nnnninfeq2  7246  prime  9492  raluz  9719  raluz2  9720  ralrp  9817  facwordi  10907  modfsummod  11844  nnwosdc  12435  isprm2  12514  isprm4  12516  metcnp  15059  limcdifap  15209  bdcriota  15957  nnnninfex  16100