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  880  pm5.6dc  916  2sb6  1972  2sb6rf  1978  2exsb  1997  mor  2056  eu2  2058  moanim  2088  r2alf  2483  r3al  2510  r19.23t  2573  ceqsralt  2753  rspc2gv  2842  ralrab  2887  ralrab2  2891  euind  2913  reu2  2914  reu3  2916  rmo4  2919  rmo3f  2923  reuind  2931  rmo2ilem  3040  rmo3  3042  ralss  3208  rabss  3219  raldifb  3262  unissb  3819  elintrab  3836  ssintrab  3847  dftr5  4083  repizf2lem  4140  reusv3  4438  tfi  4559  raliunxp  4745  fununi  5256  dff13  5736  dfsmo2  6255  tfr1onlemaccex  6316  tfrcllemaccex  6329  qliftfun  6583  nnnninfeq2  7093  prime  9290  raluz  9516  raluz2  9517  ralrp  9611  facwordi  10653  modfsummod  11399  nnwosdc  11972  isprm2  12049  isprm4  12051  metcnp  13152  limcdifap  13271  bdcriota  13765