Theorem impexp 456

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 454	. 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
2		pm3.31 455	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
3	1, 2	impbii 212	1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imdistan  578  pm4.14  819  nan  843  pm4.87  857  pm5.6  1017  2sb6  2125  r2allem  3154  r3al  3204  r19.23t  3262  ceqsralt  3488  rspc2gv  3589  ralrab  3655  ralrab2  3659  euind  3685  reu2  3686  reu3  3688  rmo4  3691  rmo3f  3695  reuind  3714  2reu5lem3  3718  rmo2  3838  rmo3  3840  rmoanim  3846  rmoanimALT  3847  ralss  3986  rabss  3998  raldifb  4088  ralin  4149  rabsssn  4629  raldifsni  4758  unissb  4904  elintrab  4923  ssintrab  4934  dftr5  5220  axrep5  5243  reusv2lem4  5368  reusv2  5370  reusv3  5372  raliunxp  5824  dfpo2  6323  fununi  6643  fvn0ssdmfun  7104  dff13  7287  ordunisuc2  7887  dfom2  7911  fnwe2lem3  8182  frpoins3xpg  8192  frpoins3xp3g  8193  xpord2indlem  8199  xpord3inddlem  8206  dfsmo2  8391  qliftfun  8859  dfsup2  9471  wemapsolem  9579  iscard2  10092  acnnum  10168  aceq1  10233  dfac9  10252  dfacacn  10257  axgroth6  10950  sstskm  10964  infm3  12314  prime  12818  raluz  13061  raluz2  13062  nnwos  13080  ralrp  13180  facwordi  14472  cotr2g  15170  rexuzre  15561  limsupgle  15685  ello12  15724  elo12  15735  lo1resb  15772  rlimresb  15773  o1resb  15774  modfsummod  16002  isprm2  16898  isprm4  16900  isprm7  16925  acsfn2  17878  pgpfac1  20338  isirred2  20693  isdomn3  21008  islindf4  22188  coe1fzgsumd  22666  evl1gsumd  22719  ist1-2  23709  isnrm2  23720  dfconn2  23781  1stccn  23826  iskgen3  23912  hausdiag  24008  cnflf  24365  txflf  24369  cnfcf  24405  metcnp  24904  caucfil  25648  ovolgelb  25845  ismbl  25891  dyadmbllem  25964  itg2leub  26099  ellimc3  26243  mdegleb  26426  jensen  27362  dchrelbas2  27610  dchrelbas3  27611  eqcuts2  28218  onsis  28706  ons2ind  28707  nmoubi  31420  nmobndseqi  31427  nmobndseqiALT  31428  h1dei  32198  nmopub  32556  nmfnleub  32573  mdsl1i  32969  mdsl2i  32970  elat2  32988  rabsspr  33185  rabsstp  33186  islinds5  34020  islbs5  34032  eulerpartlemgvv  35112  bnj115  35460  bnj1109  35521  bnj1533  35586  bnj580  35647  bnj864  35656  bnj865  35657  bnj1049  35708  bnj1090  35713  bnj1093  35714  bnj1133  35723  bnj1171  35734  climuzcnv  36637  axextprim  36674  biimpexp  36690  dfon2lem8  36760  dffun10  36884  filnetlem4  37377  mh-unprimbi  37540  bj-substax12  37834  wl-2sb6d  38751  poimirlem25  38824  poimirlem30  38829  r2alan  39442  inxpss  39508  moantr  39563  qmapeldisjsim  40051  isat3  40623  isltrn2N  41436  cdlemefrs29bpre0  41712  cdleme32fva  41753  sn-axrep5v  43531  dford4  44296  ifpidg  44747  ifpim23g  44751  elmapintrab  44832  undmrnresiss  44859  df3or2  45023  df3an2  45024  dfhe3  45030  dffrege76  45194  dffrege115  45233  ntrneiiso  45346  ismnushort  45540  pm11.62  45633  2sbc6g  45654  expcomdg  45737  impexpd  45750  dfvd2  45816  dfvd3  45828  modelac8prim  46240  rabssf  46401  2rexsb  48439  2rexrsb  48440  snlindsntor  49908  elbigo2  49989  exp12bd  50231  ralbidb  50235  ralbidc  50236  dfrals2  51308  dfralseu2  51341