Theorem simp3 1023

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 1020	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  simpl3  1026  simpr3  1029  simp3i  1032  simp3d  1035  simp13  1053  simp23  1056  simp33  1059  3anibar  1189  3ianorr  1343  intn3an3d  1392  stoic4a  1474  stoic4b  1475  mob2  2983  sotri2  5126  sotri3  5127  feq123  5465  resasplitss  5507  sefvex  5650  ftpg  5827  fsnunf  5843  fnfvima  5878  cocan1  5917  cocan2  5918  f1oiso2  5957  riotass  5990  moriotass  5991  ovmpox  6139  ovmpoga  6140  fvmpopr2d  6147  caovimo  6205  ofrval  6235  dfsmo2  6439  tfr1onlembfn  6496  tfrcllembfn  6509  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecrdg  6560  nnsucsssuc  6646  f1oen2g  6914  f1dom2g  6915  xpdom3m  7001  mapxpen  7017  diffifi  7064  unfidisj  7092  undifdc  7094  ssfidc  7107  sbthlemi9  7140  ctssdc  7288  endjudisj  7400  djuassen  7407  xpdjuen  7408  mulcanenq  7580  ltanqg  7595  addnnnq0  7644  nnanq0  7653  prltlu  7682  distrprg  7783  ltexprlemm  7795  recexprlem1ssl  7828  recexprlem1ssu  7829  addsrpr  7940  mulsrpr  7941  mulasssrg  7953  recexgt0sr  7968  ltpsrprg  7998  axmulass  8068  axpre-ltadd  8081  ltxrlt  8220  subadd2  8358  addsubass  8364  nppcan  8376  nppcan3  8378  subcan2  8379  subsub2  8382  subsub4  8387  pnpcan  8393  pnncan  8395  subcan  8409  subdi  8539  ltadd1  8584  leadd1  8585  leadd2  8586  ltsubadd  8587  ltsubadd2  8588  lesubadd  8589  lesubadd2  8590  ltaddsub  8591  leaddsub  8593  lesub1  8611  lesub2  8612  ltsub1  8613  ltsub2  8614  ltaddsublt  8726  gt0add  8728  reapadd1  8751  remulext1  8754  remulext2  8755  apadd2  8764  mulext2  8768  mulap0r  8770  leltap  8780  ltap  8788  apsub1  8797  divap0b  8838  divmulasscomap  8851  divcanap5  8869  dmdcanap  8877  redivclap  8886  div2negap  8890  lt2msq1  9040  ltdiv2  9042  ofnegsub  9117  nndivtr  9160  difgtsumgt  9524  gtndiv  9550  eluzsub  9760  nn01to3  9820  qdivcl  9846  irrmul  9850  rpgecl  9886  divge1  9927  xaddass  10073  xltadd1  10080  ubioog  10118  ubioc1  10133  lbico1  10134  iccleub  10135  lbicc2  10188  ubicc2  10189  icoshftf1o  10195  fzen  10247  elfz1b  10294  uznfz  10307  elfzo0  10390  elfzo0z  10392  ubmelfzo  10414  fzonn0p1p1  10427  ubmelm1fzo  10440  zsupssdc  10466  qbtwnre  10484  flqwordi  10516  flltdivnn0lt  10532  ceiqle  10543  modqval  10554  modqvalr  10555  modqcl  10556  flqpmodeq  10557  modq0  10559  mulqmod0  10560  negqmod0  10561  modqge0  10562  modqlt  10563  modqdiffl  10565  modqdifz  10566  modqmulnn  10572  modqvalp1  10573  modqabs2  10588  modqmuladdnn0  10598  qnegmod  10599  addmodid  10602  modqeqmodmin  10624  modfzo0difsn  10625  addmodlteq  10628  frec2uzf1od  10636  expnegap0  10777  expgt1  10807  exprecap  10810  expaddzaplem  10812  expaddzap  10813  expmulzap  10815  mulbinom2  10886  expnbnd  10893  fihashss  11046  fimaxq  11057  seq3coll  11072  swrdval  11188  swrdnd  11199  swrdlen2  11202  pfxn0  11228  ccatopth2  11257  s3cl  11326  s3fv0g  11331  s3fv1g  11332  shftfibg  11339  redivap  11393  imdivap  11400  cjdivap  11428  maxleast  11732  lemininf  11753  ltmininf  11754  bdtrilem  11758  bdtri  11759  xrmaxaddlem  11779  xrmaxadd  11780  xrmineqinf  11788  xrltmininf  11789  xrminltinf  11791  xrminadd  11794  climuni  11812  reccn2ap  11832  isumz  11908  fsumsplitsnun  11938  geoisum1c  12039  prodfap0  12064  prod1dc  12105  fprodabs  12135  cos12dec  12287  summodnegmod  12341  dvdsmultr2  12352  mulmoddvds  12382  divalglemeuneg  12442  gcdaddm  12513  gcdass  12544  mulgcd  12545  gcddiv  12548  nnminle  12564  lcmass  12615  mulgcddvds  12624  qredeq  12626  congr  12630  divgcdcoprmex  12632  cncongr1  12633  cncongr2  12634  prmexpb  12681  rpexp  12683  pythagtriplem1  12796  pythagtriplem6  12801  pythagtriplem7  12802  pythagtriplem12  12806  pythagtriplem13  12807  pythagtriplem15  12809  pythagtriplem19  12813  pcdiv  12833  dvdsprmpweqle  12868  sumhashdc  12878  pcbc  12882  4sqlem12  12933  4sqlem18  12939  unennn  12976  nninfdc  13032  fvsetsid  13074  ressressg  13116  rngmulrg  13179  imasaddvallemg  13356  qusaddvallemg  13374  mgmsscl  13402  plusfvalg  13404  ress0g  13484  imasmnd2  13493  imasmnd  13494  gsumfzz  13536  grpasscan2  13605  grpidrcan  13606  grpidlcan  13607  grpinvadd  13619  grppncan  13632  dfgrp3me  13641  grpsubpropd2  13646  pwsinvg  13653  imasgrp2  13655  imasgrp  13656  mhmmnd  13661  mulgnnsubcl  13679  mulgnn0subcl  13680  mulgsubcl  13681  mulgaddcomlem  13690  mulgaddcom  13691  mulgpropdg  13709  submmulg  13711  subgcl  13729  subgsubcl  13730  subgsub  13731  subgmulg  13733  nsgconj  13751  ghmsub  13796  ghmnsgima  13813  ghmeqker  13816  f1ghm0to0  13817  ablinvadd  13855  ablpncan2  13861  subgabl  13877  rngcl  13915  imasrng  13927  srgcl  13941  ringcl  13984  crngcom  13985  ringidss  14000  ringcom  14002  mulgass2  14029  imasring  14035  opprringbg  14051  unitmulcl  14085  unitmulclb  14086  dvrcl  14107  unitdvcl  14108  dvrcan1  14112  dvrcan3  14113  rhmmul  14136  subrngmcl  14181  subrgmcl  14205  subrgdv  14210  domneq0  14244  islmod  14263  scafvalg  14279  lmodcom  14305  lmodprop2d  14320  rmodislmodlem  14322  rmodislmod  14323  lsselg  14333  lssvnegcl  14348  lspss  14371  lspun  14374  lspsnvsi  14390  lsslsp  14401  sralmod  14422  lidlnegcl  14457  rspssp  14466  rnglidlrng  14470  qus2idrng  14497  zndvds  14621  basgen  14762  2basgeng  14764  ntrss  14801  neiss  14832  opnneiss  14840  restco  14856  restabs  14857  cnprcl2k  14888  cnpf2  14889  lmconst  14898  cnpnei  14901  cnptoprest  14921  cnmpt2t  14975  psmetsym  15011  psmetge0  15013  xmetge0  15047  xmetsym  15050  blvalps  15070  blval  15071  ssblps  15107  ssbl  15108  blpnfctr  15121  xmssym  15151  bdxmet  15183  metcnp3  15193  dvfvalap  15363  dvid  15377  dvidre  15379  dvcnp2cntop  15381  elplyr  15422  ply1term  15425  plypow  15426  ptolemy  15506  rpcxpadd  15587  rpcxpsub  15590  rpmulcxp  15591  cxpmul  15594  rpcxple2  15600  rpcxplt2  15601  cxpcom  15620  rplogbval  15627  rplogbcl  15628  rplogbchbase  15632  rplogbreexp  15635  relogbexpap  15640  logbleb  15643  logblt  15644  rplogbcxp  15645  rpcxplogb  15646  relogbcxpbap  15647  sgmppw  15674  lgslem1  15687  lgsfvalg  15692  lgsval4  15707  lgsneg  15711  lgsne0  15725  lgsdinn0  15735  lgsquad  15767  funvtxvalg  15845  funiedgvalg  15846  upgrex  15911  uhgr2edg  16012  iedginwlk  16078  upgrwlkedg  16082