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  559  nan  698  pm4.14dc  897  pm5.6dc  933  2sb6  2037  2sb6rf  2043  2exsb  2062  mor  2122  eu2  2124  moanim  2154  r2alf  2549  r3al  2576  r19.23t  2640  ceqsralt  2830  rspc2gv  2922  ralrab  2967  ralrab2  2971  euind  2993  reu2  2994  reu3  2996  rmo4  2999  rmo3f  3003  reuind  3011  rmo2ilem  3122  rmo3  3124  ralss  3293  rabss  3304  raldifb  3347  unissb  3923  elintrab  3940  ssintrab  3951  dftr5  4190  repizf2lem  4251  reusv3  4557  tfi  4680  raliunxp  4871  fununi  5398  dff13  5908  dfsmo2  6452  tfr1onlemaccex  6513  tfrcllemaccex  6526  qliftfun  6785  nnnninfeq2  7327  prime  9578  raluz  9811  raluz2  9812  ralrp  9909  facwordi  11001  modfsummod  12018  nnwosdc  12609  isprm2  12688  isprm4  12690  metcnp  15235  limcdifap  15385  bdcriota  16478  nnnninfex  16624