Theorem simp3 1001

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Proof of Theorem simp3

Step	Hyp	Ref	Expression
1		3simpc 998	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simpl3  1004  simpr3  1007  simp3i  1010  simp3d  1013  simp13  1031  simp23  1034  simp33  1037  3anibar  1167  3ianorr  1320  stoic4a  1443  stoic4b  1444  mob2  2944  sotri2  5068  sotri3  5069  feq123  5402  resasplitss  5440  sefvex  5582  ftpg  5749  fsnunf  5765  fnfvima  5800  cocan1  5837  cocan2  5838  f1oiso2  5877  riotass  5908  moriotass  5909  ovmpox  6055  ovmpoga  6056  fvmpopr2d  6063  caovimo  6121  ofrval  6150  dfsmo2  6354  tfr1onlembfn  6411  tfrcllembfn  6424  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecrdg  6475  nnsucsssuc  6559  f1oen2g  6823  f1dom2g  6824  xpdom3m  6902  mapxpen  6918  diffifi  6964  unfidisj  6992  undifdc  6994  ssfidc  7007  sbthlemi9  7040  ctssdc  7188  endjudisj  7295  djuassen  7302  xpdjuen  7303  mulcanenq  7471  ltanqg  7486  addnnnq0  7535  nnanq0  7544  prltlu  7573  distrprg  7674  ltexprlemm  7686  recexprlem1ssl  7719  recexprlem1ssu  7720  addsrpr  7831  mulsrpr  7832  mulasssrg  7844  recexgt0sr  7859  ltpsrprg  7889  axmulass  7959  axpre-ltadd  7972  ltxrlt  8111  subadd2  8249  addsubass  8255  nppcan  8267  nppcan3  8269  subcan2  8270  subsub2  8273  subsub4  8278  pnpcan  8284  pnncan  8286  subcan  8300  subdi  8430  ltadd1  8475  leadd1  8476  leadd2  8477  ltsubadd  8478  ltsubadd2  8479  lesubadd  8480  lesubadd2  8481  ltaddsub  8482  leaddsub  8484  lesub1  8502  lesub2  8503  ltsub1  8504  ltsub2  8505  ltaddsublt  8617  gt0add  8619  reapadd1  8642  remulext1  8645  remulext2  8646  apadd2  8655  mulext2  8659  mulap0r  8661  leltap  8671  ltap  8679  apsub1  8688  divap0b  8729  divmulasscomap  8742  divcanap5  8760  dmdcanap  8768  redivclap  8777  div2negap  8781  lt2msq1  8931  ltdiv2  8933  ofnegsub  9008  nndivtr  9051  difgtsumgt  9414  gtndiv  9440  eluzsub  9650  nn01to3  9710  qdivcl  9736  irrmul  9740  rpgecl  9776  divge1  9817  xaddass  9963  xltadd1  9970  ubioog  10008  ubioc1  10023  lbico1  10024  iccleub  10025  lbicc2  10078  ubicc2  10079  icoshftf1o  10085  fzen  10137  elfz1b  10184  uznfz  10197  elfzo0  10277  elfzo0z  10279  ubmelfzo  10295  fzonn0p1p1  10308  ubmelm1fzo  10321  zsupssdc  10347  qbtwnre  10365  flqwordi  10397  flltdivnn0lt  10413  ceiqle  10424  modqval  10435  modqvalr  10436  modqcl  10437  flqpmodeq  10438  modq0  10440  mulqmod0  10441  negqmod0  10442  modqge0  10443  modqlt  10444  modqdiffl  10446  modqdifz  10447  modqmulnn  10453  modqvalp1  10454  modqabs2  10469  modqmuladdnn0  10479  qnegmod  10480  addmodid  10483  modqeqmodmin  10505  modfzo0difsn  10506  addmodlteq  10509  frec2uzf1od  10517  expnegap0  10658  expgt1  10688  exprecap  10691  expaddzaplem  10693  expaddzap  10694  expmulzap  10696  mulbinom2  10767  expnbnd  10774  fihashss  10927  fimaxq  10938  seq3coll  10953  shftfibg  11004  redivap  11058  imdivap  11065  cjdivap  11093  maxleast  11397  lemininf  11418  ltmininf  11419  bdtrilem  11423  bdtri  11424  xrmaxaddlem  11444  xrmaxadd  11445  xrmineqinf  11453  xrltmininf  11454  xrminltinf  11456  xrminadd  11459  climuni  11477  reccn2ap  11497  isumz  11573  fsumsplitsnun  11603  geoisum1c  11704  prodfap0  11729  prod1dc  11770  fprodabs  11800  cos12dec  11952  summodnegmod  12006  dvdsmultr2  12017  mulmoddvds  12047  divalglemeuneg  12107  gcdaddm  12178  gcdass  12209  mulgcd  12210  gcddiv  12213  nnminle  12229  lcmass  12280  mulgcddvds  12289  qredeq  12291  congr  12295  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  prmexpb  12346  rpexp  12348  pythagtriplem1  12461  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem12  12471  pythagtriplem13  12472  pythagtriplem15  12474  pythagtriplem19  12478  pcdiv  12498  dvdsprmpweqle  12533  sumhashdc  12543  pcbc  12547  4sqlem12  12598  4sqlem18  12604  unennn  12641  nninfdc  12697  fvsetsid  12739  ressressg  12780  rngmulrg  12842  imasaddvallemg  13019  qusaddvallemg  13037  mgmsscl  13065  plusfvalg  13067  ress0g  13147  imasmnd2  13156  imasmnd  13157  gsumfzz  13199  grpasscan2  13268  grpidrcan  13269  grpidlcan  13270  grpinvadd  13282  grppncan  13295  dfgrp3me  13304  grpsubpropd2  13309  pwsinvg  13316  imasgrp2  13318  imasgrp  13319  mhmmnd  13324  mulgnnsubcl  13342  mulgnn0subcl  13343  mulgsubcl  13344  mulgaddcomlem  13353  mulgaddcom  13354  mulgpropdg  13372  submmulg  13374  subgcl  13392  subgsubcl  13393  subgsub  13394  subgmulg  13396  nsgconj  13414  ghmsub  13459  ghmnsgima  13476  ghmeqker  13479  f1ghm0to0  13480  ablinvadd  13518  ablpncan2  13524  subgabl  13540  rngcl  13578  imasrng  13590  srgcl  13604  ringcl  13647  crngcom  13648  ringidss  13663  ringcom  13665  mulgass2  13692  imasring  13698  opprringbg  13714  unitmulcl  13747  unitmulclb  13748  dvrcl  13769  unitdvcl  13770  dvrcan1  13774  dvrcan3  13775  rhmmul  13798  subrngmcl  13843  subrgmcl  13867  subrgdv  13872  domneq0  13906  islmod  13925  scafvalg  13941  lmodcom  13967  lmodprop2d  13982  rmodislmodlem  13984  rmodislmod  13985  lsselg  13995  lssvnegcl  14010  lspss  14033  lspun  14036  lspsnvsi  14052  lsslsp  14063  sralmod  14084  lidlnegcl  14119  rspssp  14128  rnglidlrng  14132  qus2idrng  14159  zndvds  14283  basgen  14424  2basgeng  14426  ntrss  14463  neiss  14494  opnneiss  14502  restco  14518  restabs  14519  cnprcl2k  14550  cnpf2  14551  lmconst  14560  cnpnei  14563  cnptoprest  14583  cnmpt2t  14637  psmetsym  14673  psmetge0  14675  xmetge0  14709  xmetsym  14712  blvalps  14732  blval  14733  ssblps  14769  ssbl  14770  blpnfctr  14783  xmssym  14813  bdxmet  14845  metcnp3  14855  dvfvalap  15025  dvid  15039  dvidre  15041  dvcnp2cntop  15043  elplyr  15084  ply1term  15087  plypow  15088  ptolemy  15168  rpcxpadd  15249  rpcxpsub  15252  rpmulcxp  15253  cxpmul  15256  rpcxple2  15262  rpcxplt2  15263  cxpcom  15282  rplogbval  15289  rplogbcl  15290  rplogbchbase  15294  rplogbreexp  15297  relogbexpap  15302  logbleb  15305  logblt  15306  rplogbcxp  15307  rpcxplogb  15308  relogbcxpbap  15309  sgmppw  15336  lgslem1  15349  lgsfvalg  15354  lgsval4  15369  lgsneg  15373  lgsne0  15387  lgsdinn0  15397  lgsquad  15429