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  807  nan  830  pm4.87  844  pm5.6  1004  2sb6  2086  r2allem  3142  r3al  3197  r19.23t  3255  moelOLD  3405  ceqsralt  3516  rspc2gv  3632  ralrab  3699  ralrab2  3704  euind  3730  reu2  3731  reu3  3733  rmo4  3736  rmo3f  3740  reuind  3759  2reu5lem3  3763  rmo2  3887  rmo3  3889  rmoanim  3894  rmoanimALT  3895  ralss  4058  ralssOLD  4060  rabss  4072  raldifb  4149  ralin  4249  rabsssn  4668  raldifsni  4795  unissb  4939  unissbOLD  4940  elintrab  4960  ssintrab  4971  dftr5  5263  dftr5OLD  5264  axrep5  5287  reusv2lem4  5401  reusv2  5403  reusv3  5405  raliunxp  5850  dfpo2  6316  fununi  6641  fvn0ssdmfun  7094  dff13  7275  ordunisuc2  7865  dfom2  7889  frpoins3xpg  8165  frpoins3xp3g  8166  xpord2indlem  8172  xpord3inddlem  8179  dfsmo2  8387  qliftfun  8842  dfsup2  9484  wemapsolem  9590  iscard2  10016  acnnum  10092  aceq1  10157  dfac9  10177  dfacacn  10182  axgroth6  10868  sstskm  10882  infm3  12227  prime  12699  raluz  12938  raluz2  12939  nnwos  12957  ralrp  13055  facwordi  14328  cotr2g  15015  rexuzre  15391  limsupgle  15513  ello12  15552  elo12  15563  lo1resb  15600  rlimresb  15601  o1resb  15602  modfsummod  15830  isprm2  16719  isprm4  16721  isprm7  16745  acsfn2  17706  pgpfac1  20100  isirred2  20421  isdomn2OLD  20712  isdomn3  20715  islindf4  21858  coe1fzgsumd  22308  evl1gsumd  22361  ist1-2  23355  isnrm2  23366  dfconn2  23427  1stccn  23471  iskgen3  23557  hausdiag  23653  cnflf  24010  txflf  24014  cnfcf  24050  metcnp  24554  caucfil  25317  ovolgelb  25515  ismbl  25561  dyadmbllem  25634  itg2leub  25769  ellimc3  25914  mdegleb  26103  jensen  27032  dchrelbas2  27281  dchrelbas3  27282  eqscut2  27851  nmoubi  30791  nmobndseqi  30798  nmobndseqiALT  30799  h1dei  31569  nmopub  31927  nmfnleub  31944  mdsl1i  32340  mdsl2i  32341  elat2  32359  rabsspr  32520  rabsstp  32521  islinds5  33395  islbs5  33408  eulerpartlemgvv  34378  bnj115  34739  bnj1109  34800  bnj1533  34866  bnj580  34927  bnj864  34936  bnj865  34937  bnj1049  34988  bnj1090  34993  bnj1093  34994  bnj1133  35003  bnj1171  35014  climuzcnv  35676  axextprim  35701  biimpexp  35717  dfon2lem8  35791  dffun10  35915  filnetlem4  36382  bj-substax12  36722  wl-2sb6d  37559  poimirlem25  37652  poimirlem30  37657  r2alan  38250  inxpss  38312  moantr  38365  isat3  39308  isltrn2N  40122  cdlemefrs29bpre0  40398  cdleme32fva  40439  sn-axrep5v  42255  dford4  43041  fnwe2lem2  43063  ifpidg  43504  ifpim23g  43508  elmapintrab  43589  undmrnresiss  43617  df3or2  43781  df3an2  43782  dfhe3  43788  dffrege76  43952  dffrege115  43991  ntrneiiso  44104  ismnushort  44320  pm11.62  44413  2sbc6g  44434  expcomdg  44520  impexpd  44533  dfvd2  44599  dfvd3  44611  modelac8prim  45009  rabssf  45124  2rexsb  47113  2rexrsb  47114  snlindsntor  48388  elbigo2  48473  exp12bd  48716  ralbidb  48720  ralbidc  48721