Theorem impexp 462

Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 10-Jan-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 460	. 2 |- ( ( ( ph /\ ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )
2		pm3.31 461	. 2 |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph /\ ps ) -> ch ) )
3	1, 2	impbii 199	1 |- ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  pm4.14  602  nan  604  pm4.87  608  imp4aOLD  615  exp4aOLD  634  imdistan  725  pm5.3  748  pm5.6  951  2sb6  2444  r2allem  2937  r3al  2940  r19.23t  3021  ceqsralt  3229  rspc2gv  3321  ralrab  3368  ralrab2  3372  euind  3393  reu2  3394  reu3  3396  rmo4  3399  reuind  3411  2reu5lem3  3415  rmo2  3526  rmo3  3528  ralss  3668  rabss  3679  raldifb  3750  rabsssn  4215  raldifsni  4324  unissb  4469  elintrab  4488  ssintrab  4500  dftr5  4755  axrep5  4776  reusv2lem4  4872  reusv2  4874  reusv3  4876  raliunxp  5261  fununi  5964  fvn0ssdmfun  6350  dff13  6512  ordunisuc2  7044  dfom2  7067  dfsmo2  7444  qliftfun  7832  dfsup2  8350  wemapsolem  8455  iscard2  8802  acnnum  8875  aceq1  8940  dfac9  8958  dfacacn  8963  axgroth6  9650  sstskm  9664  infm3  10982  prime  11458  raluz  11736  raluz2  11737  nnwos  11755  ralrp  11852  facwordi  13076  cotr2g  13715  rexuzre  14092  limsupgle  14208  ello12  14247  elo12  14258  lo1resb  14295  rlimresb  14296  o1resb  14297  modfsummod  14526  isprm2  15395  isprm4  15397  isprm7  15420  acsfn2  16324  pgpfac1  18479  isirred2  18701  isdomn2  19299  coe1fzgsumd  19672  evl1gsumd  19721  islindf4  20177  ist1-2  21151  isnrm2  21162  dfconn2  21222  1stccn  21266  iskgen3  21352  hausdiag  21448  cnflf  21806  txflf  21810  cnfcf  21846  metcnp  22346  caucfil  23081  ovolgelb  23248  ismbl  23294  dyadmbllem  23367  itg2leub  23501  ellimc3  23643  mdegleb  23824  jensen  24715  dchrelbas2  24962  dchrelbas3  24963  nmoubi  27627  nmobndseqi  27634  nmobndseqiALT  27635  h1dei  28409  nmopub  28767  nmfnleub  28784  mdsl1i  29180  mdsl2i  29181  elat2  29199  moel  29323  rmo3f  29335  rmo4fOLD  29336  eulerpartlemgvv  30438  bnj115  30791  bnj1109  30857  bnj1533  30922  bnj580  30983  bnj864  30992  bnj865  30993  bnj1049  31042  bnj1090  31047  bnj1093  31048  bnj1133  31057  bnj1171  31068  climuzcnv  31565  axextprim  31578  biimpexp  31597  dfpo2  31645  dfon2lem8  31695  dffun10  32021  filnetlem4  32376  bj-axrep5  32792  wl-2sb6d  33341  poimirlem25  33434  poimirlem30  33439  inxpss  34082  motr  34127  isat3  34594  isltrn2N  35406  cdlemefrs29bpre0  35684  cdleme32fva  35725  dford4  37596  fnwe2lem2  37621  isdomn3  37782  ifpidg  37836  ifpim23g  37840  elmapintrab  37882  undmrnresiss  37910  df3or2  38060  df3an2  38061  dfhe3  38069  dffrege76  38233  dffrege115  38272  ntrneiiso  38389  pm11.62  38594  2sbc6g  38616  expcomdg  38706  impexpd  38719  dfvd2  38795  dfvd3  38807  rabssf  39302  2rexsb  41170  2rexrsb  41171  rmoanim  41179  snlindsntor  42260  elbigo2  42346