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  806  nan  829  pm4.87  843  pm5.6  1003  2sb6  2088  r2allem  3118  r3al  3168  r19.23t  3226  ceqsralt  3469  rspc2gv  3585  ralrab  3651  ralrab2  3655  euind  3681  reu2  3682  reu3  3684  rmo4  3687  rmo3f  3691  reuind  3710  2reu5lem3  3714  rmo2  3836  rmo3  3838  rmoanim  3843  rmoanimALT  3844  ralss  4007  ralssOLD  4009  rabss  4020  raldifb  4097  ralin  4197  rabsssn  4619  raldifsni  4745  unissb  4889  elintrab  4908  ssintrab  4919  dftr5  5200  axrep5  5223  reusv2lem4  5337  reusv2  5339  reusv3  5341  raliunxp  5777  dfpo2  6239  fununi  6552  fvn0ssdmfun  7002  dff13  7183  ordunisuc2  7769  dfom2  7793  frpoins3xpg  8065  frpoins3xp3g  8066  xpord2indlem  8072  xpord3inddlem  8079  dfsmo2  8262  qliftfun  8721  dfsup2  9323  wemapsolem  9431  iscard2  9861  acnnum  9935  aceq1  10000  dfac9  10020  dfacacn  10025  axgroth6  10711  sstskm  10725  infm3  12073  prime  12546  raluz  12786  raluz2  12787  nnwos  12805  ralrp  12904  facwordi  14188  cotr2g  14875  rexuzre  15252  limsupgle  15376  ello12  15415  elo12  15426  lo1resb  15463  rlimresb  15464  o1resb  15465  modfsummod  15693  isprm2  16585  isprm4  16587  isprm7  16611  acsfn2  17561  pgpfac1  19987  isirred2  20332  isdomn2OLD  20620  isdomn3  20623  islindf4  21768  coe1fzgsumd  22212  evl1gsumd  22265  ist1-2  23255  isnrm2  23266  dfconn2  23327  1stccn  23371  iskgen3  23457  hausdiag  23553  cnflf  23910  txflf  23914  cnfcf  23950  metcnp  24449  caucfil  25203  ovolgelb  25401  ismbl  25447  dyadmbllem  25520  itg2leub  25655  ellimc3  25800  mdegleb  25989  jensen  26919  dchrelbas2  27168  dchrelbas3  27169  eqscut2  27740  onsis  28201  nmoubi  30742  nmobndseqi  30749  nmobndseqiALT  30750  h1dei  31520  nmopub  31878  nmfnleub  31895  mdsl1i  32291  mdsl2i  32292  elat2  32310  rabsspr  32471  rabsstp  32472  islinds5  33322  islbs5  33335  eulerpartlemgvv  34379  bnj115  34727  bnj1109  34788  bnj1533  34854  bnj580  34915  bnj864  34924  bnj865  34925  bnj1049  34976  bnj1090  34981  bnj1093  34982  bnj1133  34991  bnj1171  35002  climuzcnv  35683  axextprim  35713  biimpexp  35729  dfon2lem8  35803  dffun10  35927  filnetlem4  36394  bj-substax12  36734  wl-2sb6d  37571  poimirlem25  37664  poimirlem30  37669  r2alan  38263  inxpss  38324  moantr  38371  isat3  39325  isltrn2N  40138  cdlemefrs29bpre0  40414  cdleme32fva  40455  sn-axrep5v  42228  dford4  43041  fnwe2lem2  43063  ifpidg  43503  ifpim23g  43507  elmapintrab  43588  undmrnresiss  43616  df3or2  43780  df3an2  43781  dfhe3  43787  dffrege76  43951  dffrege115  43990  ntrneiiso  44103  ismnushort  44313  pm11.62  44406  2sbc6g  44427  expcomdg  44512  impexpd  44525  dfvd2  44591  dfvd3  44603  modelac8prim  45004  rabssf  45135  2rexsb  47111  2rexrsb  47112  snlindsntor  48482  elbigo2  48563  exp12bd  48806  ralbidb  48810  ralbidc  48811