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  442  pm5.3  472  pm4.87  552  nan  687  pm4.14dc  885  pm5.6dc  921  2sb6  1977  2sb6rf  1983  2exsb  2002  mor  2061  eu2  2063  moanim  2093  r2alf  2487  r3al  2514  r19.23t  2577  ceqsralt  2757  rspc2gv  2846  ralrab  2891  ralrab2  2895  euind  2917  reu2  2918  reu3  2920  rmo4  2923  rmo3f  2927  reuind  2935  rmo2ilem  3044  rmo3  3046  ralss  3213  rabss  3224  raldifb  3267  unissb  3826  elintrab  3843  ssintrab  3854  dftr5  4090  repizf2lem  4147  reusv3  4445  tfi  4566  raliunxp  4752  fununi  5266  dff13  5747  dfsmo2  6266  tfr1onlemaccex  6327  tfrcllemaccex  6340  qliftfun  6595  nnnninfeq2  7105  prime  9311  raluz  9537  raluz2  9538  ralrp  9632  facwordi  10674  modfsummod  11421  nnwosdc  11994  isprm2  12071  isprm4  12073  metcnp  13306  limcdifap  13425  bdcriota  13918