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  807  nan  830  pm4.87  844  pm5.6  1004  2sb6  2092  r2allem  3126  r3al  3176  r19.23t  3234  ceqsralt  3477  rspc2gv  3588  ralrab  3654  ralrab2  3658  euind  3684  reu2  3685  reu3  3687  rmo4  3690  rmo3f  3694  reuind  3713  2reu5lem3  3717  rmo2  3839  rmo3  3841  rmoanim  3846  rmoanimALT  3847  ralss  4010  ralssOLD  4012  rabss  4024  raldifb  4103  ralin  4203  rabsssn  4627  raldifsni  4753  unissb  4898  elintrab  4917  ssintrab  4928  dftr5  5211  axrep5  5234  reusv2lem4  5348  reusv2  5350  reusv3  5352  raliunxp  5796  dfpo2  6262  fununi  6575  fvn0ssdmfun  7028  dff13  7210  ordunisuc2  7796  dfom2  7820  frpoins3xpg  8092  frpoins3xp3g  8093  xpord2indlem  8099  xpord3inddlem  8106  dfsmo2  8289  qliftfun  8751  dfsup2  9359  wemapsolem  9467  iscard2  9900  acnnum  9974  aceq1  10039  dfac9  10059  dfacacn  10064  axgroth6  10751  sstskm  10765  infm3  12113  prime  12585  raluz  12821  raluz2  12822  nnwos  12840  ralrp  12939  facwordi  14224  cotr2g  14911  rexuzre  15288  limsupgle  15412  ello12  15451  elo12  15462  lo1resb  15499  rlimresb  15500  o1resb  15501  modfsummod  15729  isprm2  16621  isprm4  16623  isprm7  16647  acsfn2  17598  pgpfac1  20023  isirred2  20369  isdomn2OLD  20657  isdomn3  20660  islindf4  21805  coe1fzgsumd  22260  evl1gsumd  22313  ist1-2  23303  isnrm2  23314  dfconn2  23375  1stccn  23419  iskgen3  23505  hausdiag  23601  cnflf  23958  txflf  23962  cnfcf  23998  metcnp  24497  caucfil  25251  ovolgelb  25449  ismbl  25495  dyadmbllem  25568  itg2leub  25703  ellimc3  25848  mdegleb  26037  jensen  26967  dchrelbas2  27216  dchrelbas3  27217  eqcuts2  27794  onsis  28282  ons2ind  28283  nmoubi  30859  nmobndseqi  30866  nmobndseqiALT  30867  h1dei  31637  nmopub  31995  nmfnleub  32012  mdsl1i  32408  mdsl2i  32409  elat2  32427  rabsspr  32587  rabsstp  32588  islinds5  33459  islbs5  33472  eulerpartlemgvv  34553  bnj115  34901  bnj1109  34962  bnj1533  35027  bnj580  35088  bnj864  35097  bnj865  35098  bnj1049  35149  bnj1090  35154  bnj1093  35155  bnj1133  35164  bnj1171  35175  climuzcnv  35884  axextprim  35914  biimpexp  35930  dfon2lem8  36001  dffun10  36125  filnetlem4  36594  bj-substax12  36961  wl-2sb6d  37807  poimirlem25  37890  poimirlem30  37895  r2alan  38496  inxpss  38562  moantr  38617  qmapeldisjsim  39105  isat3  39677  isltrn2N  40490  cdlemefrs29bpre0  40766  cdleme32fva  40807  sn-axrep5v  42583  dford4  43380  fnwe2lem2  43402  ifpidg  43841  ifpim23g  43845  elmapintrab  43926  undmrnresiss  43954  df3or2  44118  df3an2  44119  dfhe3  44125  dffrege76  44289  dffrege115  44328  ntrneiiso  44441  ismnushort  44651  pm11.62  44744  2sbc6g  44765  expcomdg  44850  impexpd  44863  dfvd2  44929  dfvd3  44941  modelac8prim  45342  rabssf  45472  2rexsb  47455  2rexrsb  47456  snlindsntor  48825  elbigo2  48906  exp12bd  49149  ralbidb  49153  ralbidc  49154