Theorem impexp 261

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 259	. 2 |- ( ( ( ph /\ ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )
2		pm3.31 260	. 2 |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph /\ ps ) -> ch ) )
3	1, 2	impbii 125	1 |- ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imp4a  347  exp4a  364  imdistan  441  pm5.3  467  pm4.87  547  nan  682  pm4.14dc  876  pm5.6dc  912  2sb6  1964  2sb6rf  1970  2exsb  1989  mor  2048  eu2  2050  moanim  2080  r2alf  2474  r3al  2501  r19.23t  2564  ceqsralt  2739  rspc2gv  2828  ralrab  2873  ralrab2  2877  euind  2899  reu2  2900  reu3  2902  rmo4  2905  rmo3f  2909  reuind  2917  rmo2ilem  3026  rmo3  3028  ralss  3194  rabss  3205  raldifb  3247  unissb  3802  elintrab  3819  ssintrab  3830  dftr5  4065  repizf2lem  4122  reusv3  4420  tfi  4541  raliunxp  4727  fununi  5238  dff13  5718  dfsmo2  6234  tfr1onlemaccex  6295  tfrcllemaccex  6308  qliftfun  6562  nnnninfeq2  7072  prime  9263  raluz  9489  raluz2  9490  ralrp  9582  facwordi  10614  modfsummod  11355  isprm2  11993  isprm4  11995  metcnp  12912  limcdifap  13031  bdcriota  13458