Theorem impexp 443

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  imdistan  563  pm5.3  568  pm4.14  797  nan  820  pm4.87  832  pm5.6  987  2sb6  2253  r2allem  3119  r3al  3122  r19.23t  3203  ceqsralt  3431  rspc2gv  3523  ralrab  3578  ralrab2  3582  euind  3605  reu2  3606  reu3  3608  rmo4  3611  rmo3f  3615  reuind  3628  2reu5lem3  3632  rmo2  3743  rmo3  3745  rmo3OLD  3746  ralss  3889  rabss  3900  raldifb  3973  rabsssn  4436  raldifsni  4559  unissb  4706  elintrab  4724  ssintrab  4735  dftr5  4992  axrep5  5014  reusv2lem4  5115  reusv2  5117  reusv3  5119  raliunxp  5509  fununi  6211  fvn0ssdmfun  6616  dff13  6786  ordunisuc2  7324  dfom2  7347  dfsmo2  7729  qliftfun  8117  dfsup2  8640  wemapsolem  8746  iscard2  9137  acnnum  9210  aceq1  9275  dfac9  9295  dfacacn  9300  axgroth6  9987  sstskm  10001  infm3  11340  prime  11814  raluz  12046  raluz2  12047  nnwos  12066  ralrp  12163  facwordi  13398  cotr2g  14128  rexuzre  14503  limsupgle  14620  ello12  14659  elo12  14670  lo1resb  14707  rlimresb  14708  o1resb  14709  modfsummod  14934  isprm2  15804  isprm4  15806  isprm7  15828  acsfn2  16713  pgpfac1  18870  isirred2  19092  isdomn2  19700  coe1fzgsumd  20072  evl1gsumd  20121  islindf4  20585  ist1-2  21563  isnrm2  21574  dfconn2  21635  1stccn  21679  iskgen3  21765  hausdiag  21861  cnflf  22218  txflf  22222  cnfcf  22258  metcnp  22758  caucfil  23493  ovolgelb  23688  ismbl  23734  dyadmbllem  23807  itg2leub  23942  ellimc3  24084  mdegleb  24265  jensen  25171  dchrelbas2  25418  dchrelbas3  25419  nmoubi  28203  nmobndseqi  28210  nmobndseqiALT  28211  h1dei  28985  nmopub  29343  nmfnleub  29360  mdsl1i  29756  mdsl2i  29757  elat2  29775  moel  29899  islinds5  30418  eulerpartlemgvv  31040  bnj115  31397  bnj1109  31460  bnj1533  31525  bnj580  31586  bnj864  31595  bnj865  31596  bnj1049  31645  bnj1090  31650  bnj1093  31651  bnj1133  31660  bnj1171  31671  climuzcnv  32166  axextprim  32179  biimpexp  32198  dfpo2  32243  dfon2lem8  32287  dffun10  32614  filnetlem4  32968  bj-axrep5  33373  wl-2sb6d  33938  wl-dfrmosb  33991  wl-dfrmov  33992  wl-dfrmof  33993  poimirlem25  34065  poimirlem30  34070  inxpss  34716  moantr  34760  isat3  35466  isltrn2N  36279  cdlemefrs29bpre0  36555  cdleme32fva  36596  dford4  38565  fnwe2lem2  38590  isdomn3  38751  ifpidg  38804  ifpim23g  38808  elmapintrab  38849  undmrnresiss  38877  df3or2  39027  df3an2  39028  dfhe3  39035  dffrege76  39199  dffrege115  39238  ntrneiiso  39355  pm11.62  39560  2sbc6g  39581  expcomdg  39670  impexpd  39683  dfvd2  39749  dfvd3  39761  rabssf  40241  2rexsb  42139  2rexrsb  42140  rmoanim  42147  snlindsntor  43285  elbigo2  43371