Theorem impexp 451

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  imdistan  572  pm4.14  812  nan  835  pm4.87  849  pm5.6  1009  2sb6  2097  r2allem  3128  r3al  3178  r19.23t  3236  ceqsralt  3467  rspc2gv  3577  ralrab  3642  ralrab2  3646  euind  3672  reu2  3673  reu3  3675  rmo4  3678  rmo3f  3682  reuind  3701  2reu5lem3  3705  rmo2  3826  rmo3  3828  rmoanim  3833  rmoanimALT  3834  ralss  3994  ralssOLD  3996  rabss  4008  raldifb  4086  ralin  4184  rabsssn  4607  raldifsni  4735  unissb  4878  elintrab  4897  ssintrab  4908  dftr5  5190  axrep5  5214  reusv2lem4  5337  reusv2  5339  reusv3  5341  raliunxp  5788  dfpo2  6254  fununi  6567  fvn0ssdmfun  7022  dff13  7205  ordunisuc2  7791  dfom2  7815  frpoins3xpg  8087  frpoins3xp3g  8088  xpord2indlem  8094  xpord3inddlem  8101  dfsmo2  8284  qliftfun  8746  dfsup2  9354  wemapsolem  9462  iscard2  9898  acnnum  9972  aceq1  10037  dfac9  10057  dfacacn  10062  axgroth6  10749  sstskm  10763  infm3  12113  prime  12608  raluz  12844  raluz2  12845  nnwos  12863  ralrp  12962  facwordi  14249  cotr2g  14936  rexuzre  15313  limsupgle  15437  ello12  15476  elo12  15487  lo1resb  15524  rlimresb  15525  o1resb  15526  modfsummod  15755  isprm2  16649  isprm4  16651  isprm7  16676  acsfn2  17627  pgpfac1  20055  isirred2  20399  isdomn2OLD  20691  isdomn3  20694  islindf4  21820  coe1fzgsumd  22297  evl1gsumd  22350  ist1-2  23337  isnrm2  23348  dfconn2  23409  1stccn  23453  iskgen3  23539  hausdiag  23635  cnflf  23992  txflf  23996  cnfcf  24032  metcnp  24531  caucfil  25275  ovolgelb  25472  ismbl  25518  dyadmbllem  25591  itg2leub  25726  ellimc3  25871  mdegleb  26054  jensen  26977  dchrelbas2  27225  dchrelbas3  27226  eqcuts2  27803  onsis  28291  ons2ind  28292  nmoubi  30868  nmobndseqi  30875  nmobndseqiALT  30876  h1dei  31646  nmopub  32004  nmfnleub  32021  mdsl1i  32417  mdsl2i  32418  elat2  32436  rabsspr  32596  rabsstp  32597  islinds5  33457  islbs5  33470  eulerpartlemgvv  34567  bnj115  34915  bnj1109  34976  bnj1533  35041  bnj580  35102  bnj864  35111  bnj865  35112  bnj1049  35163  bnj1090  35168  bnj1093  35169  bnj1133  35178  bnj1171  35189  climuzcnv  35906  axextprim  35936  biimpexp  35952  dfon2lem8  36023  dffun10  36147  filnetlem4  36616  mh-unprimbi  36779  bj-substax12  37074  wl-2sb6d  37936  poimirlem25  38019  poimirlem30  38024  r2alan  38625  inxpss  38691  moantr  38746  qmapeldisjsim  39234  isat3  39806  isltrn2N  40619  cdlemefrs29bpre0  40895  cdleme32fva  40936  sn-axrep5v  42711  dford4  43481  fnwe2lem2  43503  ifpidg  43942  ifpim23g  43946  elmapintrab  44027  undmrnresiss  44055  df3or2  44219  df3an2  44220  dfhe3  44226  dffrege76  44390  dffrege115  44429  ntrneiiso  44542  ismnushort  44752  pm11.62  44845  2sbc6g  44866  expcomdg  44951  impexpd  44964  dfvd2  45030  dfvd3  45042  modelac8prim  45443  rabssf  45573  2rexsb  47571  2rexrsb  47572  snlindsntor  48969  elbigo2  49050  exp12bd  49293  ralbidb  49297  ralbidc  49298