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  3152  r3al  3202  r19.23t  3260  ceqsralt  3487  rspc2gv  3589  ralrab  3655  ralrab2  3659  euind  3685  reu2  3686  reu3  3688  rmo4  3691  rmo3f  3695  reuind  3714  2reu5lem3  3718  rmo2  3837  rmo3  3839  rmoanim  3845  rmoanimALT  3846  ralss  4007  ralssOLD  4009  rabss  4021  raldifb  4099  ralin  4198  rabsssn  4632  raldifsni  4761  unissb  4904  elintrab  4923  ssintrab  4934  dftr5  5220  axrep5  5244  reusv2lem4  5370  reusv2  5372  reusv3  5374  raliunxp  5823  dfpo2  6298  fununi  6612  fvn0ssdmfun  7070  dff13  7254  ordunisuc2  7843  dfom2  7867  frpoins3xpg  8141  frpoins3xp3g  8142  xpord2indlem  8148  xpord3inddlem  8155  dfsmo2  8339  qliftfun  8805  dfsup2  9417  wemapsolem  9525  iscard2  9984  acnnum  10058  aceq1  10123  dfac9  10142  dfacacn  10147  axgroth6  10840  sstskm  10854  infm3  12201  prime  12705  raluz  12948  raluz2  12949  nnwos  12967  ralrp  13066  facwordi  14355  cotr2g  15051  rexuzre  15442  limsupgle  15566  ello12  15605  elo12  15616  lo1resb  15653  rlimresb  15654  o1resb  15655  modfsummod  15883  isprm2  16776  isprm4  16778  isprm7  16803  acsfn2  17755  pgpfac1  20213  isirred2  20566  isdomn3  20880  islindf4  22055  coe1fzgsumd  22533  evl1gsumd  22586  ist1-2  23576  isnrm2  23587  dfconn2  23648  1stccn  23693  iskgen3  23779  hausdiag  23875  cnflf  24232  txflf  24236  cnfcf  24272  metcnp  24771  caucfil  25515  ovolgelb  25712  ismbl  25758  dyadmbllem  25831  itg2leub  25966  ellimc3  26111  mdegleb  26294  jensen  27226  dchrelbas2  27474  dchrelbas3  27475  eqcuts2  28052  onsis  28540  ons2ind  28541  nmoubi  31254  nmobndseqi  31261  nmobndseqiALT  31262  h1dei  32032  nmopub  32390  nmfnleub  32407  mdsl1i  32803  mdsl2i  32804  elat2  32822  rabsspr  32977  rabsstp  32978  islinds5  33804  islbs5  33815  eulerpartlemgvv  34889  bnj115  35237  bnj1109  35298  bnj1533  35363  bnj580  35424  bnj864  35433  bnj865  35434  bnj1049  35485  bnj1090  35490  bnj1093  35491  bnj1133  35500  bnj1171  35511  climuzcnv  36252  axextprim  36282  biimpexp  36298  dfon2lem8  36369  dffun10  36493  filnetlem4  37002  mh-unprimbi  37165  bj-substax12  37459  wl-2sb6d  38323  poimirlem25  38396  poimirlem30  38401  r2alan  39001  inxpss  39067  moantr  39122  qmapeldisjsim  39610  isat3  40182  isltrn2N  40995  cdlemefrs29bpre0  41271  cdleme32fva  41312  sn-axrep5v  43089  dford4  43872  fnwe2lem2  43894  ifpidg  44333  ifpim23g  44337  elmapintrab  44418  undmrnresiss  44446  df3or2  44610  df3an2  44611  dfhe3  44617  dffrege76  44781  dffrege115  44820  ntrneiiso  44933  ismnushort  45127  pm11.62  45220  2sbc6g  45241  expcomdg  45325  impexpd  45338  dfvd2  45404  dfvd3  45416  modelac8prim  45817  rabssf  45953  2rexsb  47991  2rexrsb  47992  snlindsntor  49403  elbigo2  49484  exp12bd  49726  ralbidb  49730  ralbidc  49731  dfrals2  50721  dfralseu2  50754