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 208	1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  imdistan  568  pm4.14  804  nan  827  pm4.87  840  pm5.6  999  2sb6  2088  r2allem  3135  r3al  3189  r19.23t  3234  moelOLD  3374  ceqsralt  3472  rspc2gv  3578  ralrab  3640  ralrab2  3645  euind  3670  reu2  3671  reu3  3673  rmo4  3676  rmo3f  3680  reuind  3699  2reu5lem3  3703  rmo2  3831  rmo3  3833  rmoanim  3838  rmoanimALT  3839  ralss  4002  rabss  4017  raldifb  4091  rabsssn  4615  raldifsni  4742  unissb  4887  unissbOLD  4888  elintrab  4908  ssintrab  4919  dftr5  5213  dftr5OLD  5214  axrep5  5235  reusv2lem4  5344  reusv2  5346  reusv3  5348  raliunxp  5781  dfpo2  6234  fununi  6559  fvn0ssdmfun  7008  dff13  7184  ordunisuc2  7758  dfom2  7782  dfsmo2  8248  qliftfun  8662  dfsup2  9301  wemapsolem  9407  iscard2  9833  acnnum  9909  aceq1  9974  dfac9  9993  dfacacn  9998  axgroth6  10685  sstskm  10699  infm3  12035  prime  12502  raluz  12737  raluz2  12738  nnwos  12756  ralrp  12851  facwordi  14104  cotr2g  14786  rexuzre  15163  limsupgle  15285  ello12  15324  elo12  15335  lo1resb  15372  rlimresb  15373  o1resb  15374  modfsummod  15605  isprm2  16484  isprm4  16486  isprm7  16510  acsfn2  17469  pgpfac1  19778  isirred2  20038  isdomn2  20676  islindf4  21151  coe1fzgsumd  21579  evl1gsumd  21629  ist1-2  22604  isnrm2  22615  dfconn2  22676  1stccn  22720  iskgen3  22806  hausdiag  22902  cnflf  23259  txflf  23263  cnfcf  23299  metcnp  23803  caucfil  24553  ovolgelb  24750  ismbl  24796  dyadmbllem  24869  itg2leub  25005  ellimc3  25149  mdegleb  25335  jensen  26244  dchrelbas2  26491  dchrelbas3  26492  eqscut2  27051  nmoubi  29422  nmobndseqi  29429  nmobndseqiALT  29430  h1dei  30200  nmopub  30558  nmfnleub  30575  mdsl1i  30971  mdsl2i  30972  elat2  30990  islinds5  31860  eulerpartlemgvv  32643  bnj115  33004  bnj1109  33065  bnj1533  33131  bnj580  33192  bnj864  33201  bnj865  33202  bnj1049  33253  bnj1090  33258  bnj1093  33259  bnj1133  33268  bnj1171  33279  climuzcnv  33928  axextprim  33941  biimpexp  33957  dfon2lem8  34049  frpoins3xpg  34069  frpoins3xp3g  34070  xpord2ind  34076  xpord3ind  34082  dffun10  34312  filnetlem4  34666  bj-substax12  34999  wl-2sb6d  35818  poimirlem25  35907  poimirlem30  35912  ralin  36511  r2alan  36512  inxpss  36577  moantr  36630  isat3  37574  isltrn2N  38388  cdlemefrs29bpre0  38664  cdleme32fva  38705  sn-axrep5v  40442  dford4  41114  fnwe2lem2  41139  isdomn3  41292  ifpidg  41420  ifpim23g  41424  elmapintrab  41505  undmrnresiss  41533  df3or2  41697  df3an2  41698  dfhe3  41704  dffrege76  41868  dffrege115  41907  ntrneiiso  42022  ismnushort  42240  pm11.62  42333  2sbc6g  42354  expcomdg  42441  impexpd  42454  dfvd2  42520  dfvd3  42532  rabssf  42989  2rexsb  44944  2rexrsb  44945  snlindsntor  46163  elbigo2  46249  exp12bd  46492  ralbidb  46496  ralbidc  46497