Theorem impexp 250

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 248	. 2 |- ( ( ( ph /\ ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )
2		pm3.31 249	. 2 |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph /\ ps ) -> ch ) )
3	1, 2	impbii 117	1 |- ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) )

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  imp4a  331  exp4a  348  imdistan  418  pm5.3  444  pm4.87  493  nan  626  pm4.14dc  787  pm5.6dc  835  2sb6  1860  2sb6rf  1866  2exsb  1885  mor  1942  eu2  1944  moanim  1974  r2alf  2341  r3al  2366  r19.23t  2423  ceqsralt  2581  ralrab  2702  ralrab2  2706  euind  2728  reu2  2729  reu3  2731  rmo4  2734  reuind  2744  rmo2ilem  2847  rmo3  2849  ralss  3006  rabss  3017  raldifb  3083  unissb  3610  elintrab  3627  ssintrab  3638  dftr5  3857  repizf2lem  3914  reusv3  4192  tfi  4305  raliunxp  4477  fununi  4967  dff13  5407  dfsmo2  5902  qliftfun  6188  prime  8337  raluz  8521  raluz2  8522  ralrp  8604  bdcriota  10003