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  699  pm4.14dc  898  pm5.6dc  934  2sb6  2038  2sb6rf  2044  2exsb  2063  mor  2123  eu2  2125  moanim  2155  r2alf  2559  r3al  2586  r19.23t  2650  ceqsralt  2841  rspc2gv  2933  ralrab  2978  ralrab2  2982  euind  3004  reu2  3005  reu3  3007  rmo4  3010  rmo3f  3014  reuind  3022  rmo2ilem  3133  rmo3  3135  ralss  3304  rabss  3315  raldifb  3359  unissb  3944  elintrab  3961  ssintrab  3972  dftr5  4211  repizf2lem  4274  reusv3  4581  tfi  4704  raliunxp  4896  fununi  5424  dff13  5941  dfsmo2  6518  tfr1onlemaccex  6579  tfrcllemaccex  6592  qliftfun  6851  nnnninfeq2  7420  prime  9677  raluz  9910  raluz2  9911  ralrp  10008  facwordi  11102  modfsummod  12144  nnwosdc  12735  isprm2  12814  isprm4  12816  metcnp  15377  limcdifap  15527  bdcriota  16653  nnnninfex  16800