Theorem impexp 450

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	⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Proof of Theorem impexp

Step	Hyp	Ref	Expression
1		pm3.3 448	. 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
2		pm3.31 449	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
3	1, 2	impbii 209	1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  imdistan  567  pm4.14  806  nan  829  pm4.87  843  pm5.6  1003  2sb6  2087  r2allem  3117  r3al  3167  r19.23t  3225  ceqsralt  3473  rspc2gv  3589  ralrab  3656  ralrab2  3660  euind  3686  reu2  3687  reu3  3689  rmo4  3692  rmo3f  3696  reuind  3715  2reu5lem3  3719  rmo2  3841  rmo3  3843  rmoanim  3848  rmoanimALT  3849  ralss  4012  ralssOLD  4014  rabss  4025  raldifb  4102  ralin  4202  rabsssn  4622  raldifsni  4749  unissb  4893  elintrab  4913  ssintrab  4924  dftr5  5206  axrep5  5229  reusv2lem4  5343  reusv2  5345  reusv3  5347  raliunxp  5786  dfpo2  6248  fununi  6561  fvn0ssdmfun  7012  dff13  7195  ordunisuc2  7784  dfom2  7808  frpoins3xpg  8080  frpoins3xp3g  8081  xpord2indlem  8087  xpord3inddlem  8094  dfsmo2  8277  qliftfun  8736  dfsup2  9353  wemapsolem  9461  iscard2  9891  acnnum  9965  aceq1  10030  dfac9  10050  dfacacn  10055  axgroth6  10741  sstskm  10755  infm3  12102  prime  12575  raluz  12815  raluz2  12816  nnwos  12834  ralrp  12933  facwordi  14214  cotr2g  14901  rexuzre  15278  limsupgle  15402  ello12  15441  elo12  15452  lo1resb  15489  rlimresb  15490  o1resb  15491  modfsummod  15719  isprm2  16611  isprm4  16613  isprm7  16637  acsfn2  17587  pgpfac1  19979  isirred2  20324  isdomn2OLD  20615  isdomn3  20618  islindf4  21763  coe1fzgsumd  22207  evl1gsumd  22260  ist1-2  23250  isnrm2  23261  dfconn2  23322  1stccn  23366  iskgen3  23452  hausdiag  23548  cnflf  23905  txflf  23909  cnfcf  23945  metcnp  24445  caucfil  25199  ovolgelb  25397  ismbl  25443  dyadmbllem  25516  itg2leub  25651  ellimc3  25796  mdegleb  25985  jensen  26915  dchrelbas2  27164  dchrelbas3  27165  eqscut2  27735  onsis  28195  nmoubi  30734  nmobndseqi  30741  nmobndseqiALT  30742  h1dei  31512  nmopub  31870  nmfnleub  31887  mdsl1i  32283  mdsl2i  32284  elat2  32302  rabsspr  32463  rabsstp  32464  islinds5  33314  islbs5  33327  eulerpartlemgvv  34343  bnj115  34691  bnj1109  34752  bnj1533  34818  bnj580  34879  bnj864  34888  bnj865  34889  bnj1049  34940  bnj1090  34945  bnj1093  34946  bnj1133  34955  bnj1171  34966  climuzcnv  35643  axextprim  35673  biimpexp  35689  dfon2lem8  35763  dffun10  35887  filnetlem4  36354  bj-substax12  36694  wl-2sb6d  37531  poimirlem25  37624  poimirlem30  37629  r2alan  38223  inxpss  38284  moantr  38331  isat3  39285  isltrn2N  40099  cdlemefrs29bpre0  40375  cdleme32fva  40416  sn-axrep5v  42189  dford4  43002  fnwe2lem2  43024  ifpidg  43464  ifpim23g  43468  elmapintrab  43549  undmrnresiss  43577  df3or2  43741  df3an2  43742  dfhe3  43748  dffrege76  43912  dffrege115  43951  ntrneiiso  44064  ismnushort  44274  pm11.62  44367  2sbc6g  44388  expcomdg  44474  impexpd  44487  dfvd2  44553  dfvd3  44565  modelac8prim  44966  rabssf  45097  2rexsb  47086  2rexrsb  47087  snlindsntor  48457  elbigo2  48538  exp12bd  48781  ralbidb  48785  ralbidc  48786