Theorem impexp 453

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  imdistan  570  pm4.14  805  nan  827  pm4.87  839  pm5.6  998  2sb6  2094  r2allem  3200  r3al  3202  r19.23t  3313  ceqsralt  3528  rspc2gv  3632  ralrab  3685  ralrab2  3690  euind  3715  reu2  3716  reu3  3718  rmo4  3721  rmo3f  3725  reuind  3744  2reu5lem3  3748  rmo2  3870  rmo3  3872  rmo3OLD  3873  rmoanim  3878  rmoanimALT  3879  ralss  4037  rabss  4048  raldifb  4121  rabsssn  4607  raldifsni  4728  unissb  4870  elintrab  4888  ssintrab  4899  dftr5  5175  axrep5  5196  reusv2lem4  5302  reusv2  5304  reusv3  5306  raliunxp  5710  fununi  6429  fvn0ssdmfun  6842  dff13  7013  ordunisuc2  7559  dfom2  7582  dfsmo2  7984  qliftfun  8382  dfsup2  8908  wemapsolem  9014  iscard2  9405  acnnum  9478  aceq1  9543  dfac9  9562  dfacacn  9567  axgroth6  10250  sstskm  10264  infm3  11600  prime  12064  raluz  12297  raluz2  12298  nnwos  12316  ralrp  12410  facwordi  13650  cotr2g  14336  rexuzre  14712  limsupgle  14834  ello12  14873  elo12  14884  lo1resb  14921  rlimresb  14922  o1resb  14923  modfsummod  15149  isprm2  16026  isprm4  16028  isprm7  16052  acsfn2  16934  pgpfac1  19202  isirred2  19451  isdomn2  20072  coe1fzgsumd  20470  evl1gsumd  20520  islindf4  20982  ist1-2  21955  isnrm2  21966  dfconn2  22027  1stccn  22071  iskgen3  22157  hausdiag  22253  cnflf  22610  txflf  22614  cnfcf  22650  metcnp  23151  caucfil  23886  ovolgelb  24081  ismbl  24127  dyadmbllem  24200  itg2leub  24335  ellimc3  24477  mdegleb  24658  jensen  25566  dchrelbas2  25813  dchrelbas3  25814  nmoubi  28549  nmobndseqi  28556  nmobndseqiALT  28557  h1dei  29327  nmopub  29685  nmfnleub  29702  mdsl1i  30098  mdsl2i  30099  elat2  30117  moel  30252  islinds5  30932  eulerpartlemgvv  31634  bnj115  31995  bnj1109  32058  bnj1533  32124  bnj580  32185  bnj864  32194  bnj865  32195  bnj1049  32246  bnj1090  32251  bnj1093  32252  bnj1133  32261  bnj1171  32272  climuzcnv  32914  axextprim  32927  biimpexp  32946  dfpo2  32991  dfon2lem8  33035  dffun10  33375  filnetlem4  33729  wl-2sb6d  34809  wl-dfrmosb  34868  wl-dfrmov  34869  wl-dfrmof  34870  poimirlem25  34932  poimirlem30  34937  inxpss  35584  moantr  35631  isat3  36458  isltrn2N  37271  cdlemefrs29bpre0  37547  cdleme32fva  37588  sn-axrep5v  39157  dford4  39675  fnwe2lem2  39700  isdomn3  39853  ifpidg  39906  ifpim23g  39910  elmapintrab  39985  undmrnresiss  40013  df3or2  40162  df3an2  40163  dfhe3  40170  dffrege76  40334  dffrege115  40373  ntrneiiso  40490  pm11.62  40775  2sbc6g  40796  expcomdg  40883  impexpd  40896  dfvd2  40962  dfvd3  40974  rabssf  41434  2rexsb  43348  2rexrsb  43349  snlindsntor  44575  elbigo2  44661