Theorem impexp 454

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  imdistan  571  pm4.14  806  nan  828  pm4.87  840  pm5.6  999  2sb6  2091  r2allem  3165  r3al  3167  r19.23t  3272  ceqsralt  3475  rspc2gv  3580  ralrab  3633  ralrab2  3638  euind  3663  reu2  3664  reu3  3666  rmo4  3669  rmo3f  3673  reuind  3692  2reu5lem3  3696  rmo2  3816  rmo3  3818  rmoanim  3823  rmoanimALT  3824  ralss  3985  rabss  3999  raldifb  4072  rabsssn  4567  raldifsni  4688  unissb  4832  elintrab  4850  ssintrab  4861  dftr5  5139  axrep5  5160  reusv2lem4  5267  reusv2  5269  reusv3  5271  raliunxp  5674  fununi  6399  fvn0ssdmfun  6819  dff13  6991  ordunisuc2  7539  dfom2  7562  dfsmo2  7967  qliftfun  8365  dfsup2  8892  wemapsolem  8998  iscard2  9389  acnnum  9463  aceq1  9528  dfac9  9547  dfacacn  9552  axgroth6  10239  sstskm  10253  infm3  11587  prime  12051  raluz  12284  raluz2  12285  nnwos  12303  ralrp  12397  facwordi  13645  cotr2g  14327  rexuzre  14704  limsupgle  14826  ello12  14865  elo12  14876  lo1resb  14913  rlimresb  14914  o1resb  14915  modfsummod  15141  isprm2  16016  isprm4  16018  isprm7  16042  acsfn2  16926  pgpfac1  19195  isirred2  19447  isdomn2  20065  islindf4  20527  coe1fzgsumd  20931  evl1gsumd  20981  ist1-2  21952  isnrm2  21963  dfconn2  22024  1stccn  22068  iskgen3  22154  hausdiag  22250  cnflf  22607  txflf  22611  cnfcf  22647  metcnp  23148  caucfil  23887  ovolgelb  24084  ismbl  24130  dyadmbllem  24203  itg2leub  24338  ellimc3  24482  mdegleb  24665  jensen  25574  dchrelbas2  25821  dchrelbas3  25822  nmoubi  28555  nmobndseqi  28562  nmobndseqiALT  28563  h1dei  29333  nmopub  29691  nmfnleub  29708  mdsl1i  30104  mdsl2i  30105  elat2  30123  moel  30259  islinds5  30983  eulerpartlemgvv  31744  bnj115  32105  bnj1109  32168  bnj1533  32234  bnj580  32295  bnj864  32304  bnj865  32305  bnj1049  32356  bnj1090  32361  bnj1093  32362  bnj1133  32371  bnj1171  32382  climuzcnv  33027  axextprim  33040  biimpexp  33059  dfpo2  33104  dfon2lem8  33148  dffun10  33488  filnetlem4  33842  bj-subst  34168  wl-2sb6d  34959  wl-dfrmosb  35018  wl-dfrmov  35019  wl-dfrmof  35020  poimirlem25  35082  poimirlem30  35087  inxpss  35729  moantr  35776  isat3  36603  isltrn2N  37416  cdlemefrs29bpre0  37692  cdleme32fva  37733  sn-axrep5v  39400  dford4  39970  fnwe2lem2  39995  isdomn3  40148  ifpidg  40199  ifpim23g  40203  elmapintrab  40276  undmrnresiss  40304  df3or2  40469  df3an2  40470  dfhe3  40476  dffrege76  40640  dffrege115  40679  ntrneiiso  40794  pm11.62  41098  2sbc6g  41119  expcomdg  41206  impexpd  41219  dfvd2  41285  dfvd3  41297  rabssf  41754  2rexsb  43656  2rexrsb  43657  snlindsntor  44880  elbigo2  44966