Theorem impexp 456

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imdistan  578  pm4.14  819  nan  843  pm4.87  857  pm5.6  1017  2sb6  2123  r2allem  3150  r3al  3200  r19.23t  3258  ceqsralt  3484  rspc2gv  3586  ralrab  3652  ralrab2  3656  euind  3682  reu2  3683  reu3  3685  rmo4  3688  rmo3f  3692  reuind  3711  2reu5lem3  3715  rmo2  3834  rmo3  3836  rmoanim  3842  rmoanimALT  3843  ralss  4004  ralssOLD  4006  rabss  4018  raldifb  4096  ralin  4195  rabsssn  4629  raldifsni  4758  unissb  4901  elintrab  4920  ssintrab  4931  dftr5  5216  axrep5  5240  reusv2lem4  5366  reusv2  5368  reusv3  5370  raliunxp  5819  dfpo2  6294  fununi  6608  fvn0ssdmfun  7067  dff13  7251  ordunisuc2  7840  dfom2  7864  frpoins3xpg  8138  frpoins3xp3g  8139  xpord2indlem  8145  xpord3inddlem  8152  dfsmo2  8336  qliftfun  8802  dfsup2  9414  wemapsolem  9522  iscard2  9981  acnnum  10055  aceq1  10120  dfac9  10139  dfacacn  10144  axgroth6  10837  sstskm  10851  infm3  12198  prime  12702  raluz  12945  raluz2  12946  nnwos  12964  ralrp  13064  facwordi  14353  cotr2g  15049  rexuzre  15440  limsupgle  15564  ello12  15603  elo12  15614  lo1resb  15651  rlimresb  15652  o1resb  15653  modfsummod  15881  isprm2  16772  isprm4  16774  isprm7  16799  acsfn2  17751  pgpfac1  20209  isirred2  20562  isdomn3  20876  islindf4  22051  coe1fzgsumd  22529  evl1gsumd  22582  ist1-2  23572  isnrm2  23583  dfconn2  23644  1stccn  23689  iskgen3  23775  hausdiag  23871  cnflf  24228  txflf  24232  cnfcf  24268  metcnp  24767  caucfil  25511  ovolgelb  25708  ismbl  25754  dyadmbllem  25827  itg2leub  25962  ellimc3  26106  mdegleb  26289  jensen  27225  dchrelbas2  27473  dchrelbas3  27474  eqcuts2  28051  onsis  28539  ons2ind  28540  nmoubi  31253  nmobndseqi  31260  nmobndseqiALT  31261  h1dei  32031  nmopub  32389  nmfnleub  32406  mdsl1i  32802  mdsl2i  32803  elat2  32821  rabsspr  32976  rabsstp  32977  islinds5  33802  islbs5  33813  eulerpartlemgvv  34887  bnj115  35235  bnj1109  35296  bnj1533  35361  bnj580  35422  bnj864  35431  bnj865  35432  bnj1049  35483  bnj1090  35488  bnj1093  35489  bnj1133  35498  bnj1171  35509  climuzcnv  36250  axextprim  36280  biimpexp  36296  dfon2lem8  36367  dffun10  36491  filnetlem4  37000  mh-unprimbi  37163  bj-substax12  37457  wl-2sb6d  38321  poimirlem25  38394  poimirlem30  38399  r2alan  38999  inxpss  39065  moantr  39120  qmapeldisjsim  39608  isat3  40180  isltrn2N  40993  cdlemefrs29bpre0  41269  cdleme32fva  41310  sn-axrep5v  43087  dford4  43870  fnwe2lem2  43892  ifpidg  44331  ifpim23g  44335  elmapintrab  44416  undmrnresiss  44444  df3or2  44608  df3an2  44609  dfhe3  44615  dffrege76  44779  dffrege115  44818  ntrneiiso  44931  ismnushort  45125  pm11.62  45218  2sbc6g  45239  expcomdg  45323  impexpd  45336  dfvd2  45402  dfvd3  45414  modelac8prim  45815  rabssf  45951  2rexsb  47989  2rexrsb  47990  snlindsntor  49401  elbigo2  49482  exp12bd  49724  ralbidb  49728  ralbidc  49729  dfrals2  50719  dfralseu2  50752