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  2092  r2allem  3125  r3al  3175  r19.23t  3233  ceqsralt  3464  rspc2gv  3574  ralrab  3640  ralrab2  3644  euind  3670  reu2  3671  reu3  3673  rmo4  3676  rmo3f  3680  reuind  3699  2reu5lem3  3703  rmo2  3825  rmo3  3827  rmoanim  3832  rmoanimALT  3833  ralss  3996  ralssOLD  3998  rabss  4010  raldifb  4089  ralin  4189  rabsssn  4612  raldifsni  4740  unissb  4883  elintrab  4902  ssintrab  4913  dftr5  5196  axrep5  5220  reusv2lem4  5343  reusv2  5345  reusv3  5347  raliunxp  5794  dfpo2  6260  fununi  6573  fvn0ssdmfun  7026  dff13  7209  ordunisuc2  7795  dfom2  7819  frpoins3xpg  8090  frpoins3xp3g  8091  xpord2indlem  8097  xpord3inddlem  8104  dfsmo2  8287  qliftfun  8749  dfsup2  9357  wemapsolem  9465  iscard2  9900  acnnum  9974  aceq1  10039  dfac9  10059  dfacacn  10064  axgroth6  10751  sstskm  10765  infm3  12115  prime  12610  raluz  12846  raluz2  12847  nnwos  12865  ralrp  12964  facwordi  14251  cotr2g  14938  rexuzre  15315  limsupgle  15439  ello12  15478  elo12  15489  lo1resb  15526  rlimresb  15527  o1resb  15528  modfsummod  15757  isprm2  16651  isprm4  16653  isprm7  16678  acsfn2  17629  pgpfac1  20057  isirred2  20401  isdomn2OLD  20689  isdomn3  20692  islindf4  21818  coe1fzgsumd  22269  evl1gsumd  22322  ist1-2  23312  isnrm2  23323  dfconn2  23384  1stccn  23428  iskgen3  23514  hausdiag  23610  cnflf  23967  txflf  23971  cnfcf  24007  metcnp  24506  caucfil  25250  ovolgelb  25447  ismbl  25493  dyadmbllem  25566  itg2leub  25701  ellimc3  25846  mdegleb  26029  jensen  26952  dchrelbas2  27200  dchrelbas3  27201  eqcuts2  27778  onsis  28266  ons2ind  28267  nmoubi  30843  nmobndseqi  30850  nmobndseqiALT  30851  h1dei  31621  nmopub  31979  nmfnleub  31996  mdsl1i  32392  mdsl2i  32393  elat2  32411  rabsspr  32571  rabsstp  32572  islinds5  33427  islbs5  33440  eulerpartlemgvv  34520  bnj115  34868  bnj1109  34929  bnj1533  34994  bnj580  35055  bnj864  35064  bnj865  35065  bnj1049  35116  bnj1090  35121  bnj1093  35122  bnj1133  35131  bnj1171  35142  climuzcnv  35853  axextprim  35883  biimpexp  35899  dfon2lem8  35970  dffun10  36094  filnetlem4  36563  mh-unprimbi  36726  bj-substax12  37021  wl-2sb6d  37883  poimirlem25  37966  poimirlem30  37971  r2alan  38572  inxpss  38638  moantr  38693  qmapeldisjsim  39181  isat3  39753  isltrn2N  40566  cdlemefrs29bpre0  40842  cdleme32fva  40883  sn-axrep5v  42658  dford4  43457  fnwe2lem2  43479  ifpidg  43918  ifpim23g  43922  elmapintrab  44003  undmrnresiss  44031  df3or2  44195  df3an2  44196  dfhe3  44202  dffrege76  44366  dffrege115  44405  ntrneiiso  44518  ismnushort  44728  pm11.62  44821  2sbc6g  44842  expcomdg  44927  impexpd  44940  dfvd2  45006  dfvd3  45018  modelac8prim  45419  rabssf  45549  2rexsb  47549  2rexrsb  47550  snlindsntor  48947  elbigo2  49028  exp12bd  49271  ralbidb  49275  ralbidc  49276