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  5067  sotri3  5068  feq123  5399  resasplitss  5437  sefvex  5579  ftpg  5746  fsnunf  5762  fnfvima  5797  cocan1  5834  cocan2  5835  f1oiso2  5874  riotass  5905  moriotass  5906  ovmpox  6051  ovmpoga  6052  fvmpopr2d  6059  caovimo  6117  ofrval  6146  dfsmo2  6345  tfr1onlembfn  6402  tfrcllembfn  6415  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecrdg  6466  nnsucsssuc  6550  f1oen2g  6814  f1dom2g  6815  xpdom3m  6893  mapxpen  6909  diffifi  6955  unfidisj  6983  undifdc  6985  ssfidc  6998  sbthlemi9  7031  ctssdc  7179  endjudisj  7277  djuassen  7284  xpdjuen  7285  mulcanenq  7452  ltanqg  7467  addnnnq0  7516  nnanq0  7525  prltlu  7554  distrprg  7655  ltexprlemm  7667  recexprlem1ssl  7700  recexprlem1ssu  7701  addsrpr  7812  mulsrpr  7813  mulasssrg  7825  recexgt0sr  7840  ltpsrprg  7870  axmulass  7940  axpre-ltadd  7953  ltxrlt  8092  subadd2  8230  addsubass  8236  nppcan  8248  nppcan3  8250  subcan2  8251  subsub2  8254  subsub4  8259  pnpcan  8265  pnncan  8267  subcan  8281  subdi  8411  ltadd1  8456  leadd1  8457  leadd2  8458  ltsubadd  8459  ltsubadd2  8460  lesubadd  8461  lesubadd2  8462  ltaddsub  8463  leaddsub  8465  lesub1  8483  lesub2  8484  ltsub1  8485  ltsub2  8486  ltaddsublt  8598  gt0add  8600  reapadd1  8623  remulext1  8626  remulext2  8627  apadd2  8636  mulext2  8640  mulap0r  8642  leltap  8652  ltap  8660  apsub1  8669  divap0b  8710  divmulasscomap  8723  divcanap5  8741  dmdcanap  8749  redivclap  8758  div2negap  8762  lt2msq1  8912  ltdiv2  8914  ofnegsub  8989  nndivtr  9032  difgtsumgt  9395  gtndiv  9421  eluzsub  9631  nn01to3  9691  qdivcl  9717  irrmul  9721  rpgecl  9757  divge1  9798  xaddass  9944  xltadd1  9951  ubioog  9989  ubioc1  10004  lbico1  10005  iccleub  10006  lbicc2  10059  ubicc2  10060  icoshftf1o  10066  fzen  10118  elfz1b  10165  uznfz  10178  elfzo0  10258  elfzo0z  10260  ubmelfzo  10276  fzonn0p1p1  10289  ubmelm1fzo  10302  zsupssdc  10328  qbtwnre  10346  flqwordi  10378  flltdivnn0lt  10394  ceiqle  10405  modqval  10416  modqvalr  10417  modqcl  10418  flqpmodeq  10419  modq0  10421  mulqmod0  10422  negqmod0  10423  modqge0  10424  modqlt  10425  modqdiffl  10427  modqdifz  10428  modqmulnn  10434  modqvalp1  10435  modqabs2  10450  modqmuladdnn0  10460  qnegmod  10461  addmodid  10464  modqeqmodmin  10486  modfzo0difsn  10487  addmodlteq  10490  frec2uzf1od  10498  expnegap0  10639  expgt1  10669  exprecap  10672  expaddzaplem  10674  expaddzap  10675  expmulzap  10677  mulbinom2  10748  expnbnd  10755  fihashss  10908  fimaxq  10919  seq3coll  10934  shftfibg  10985  redivap  11039  imdivap  11046  cjdivap  11074  maxleast  11378  lemininf  11399  ltmininf  11400  bdtrilem  11404  bdtri  11405  xrmaxaddlem  11425  xrmaxadd  11426  xrmineqinf  11434  xrltmininf  11435  xrminltinf  11437  xrminadd  11440  climuni  11458  reccn2ap  11478  isumz  11554  fsumsplitsnun  11584  geoisum1c  11685  prodfap0  11710  prod1dc  11751  fprodabs  11781  cos12dec  11933  summodnegmod  11987  dvdsmultr2  11998  mulmoddvds  12028  divalglemeuneg  12088  gcdaddm  12151  gcdass  12182  mulgcd  12183  gcddiv  12186  nnminle  12202  lcmass  12253  mulgcddvds  12262  qredeq  12264  congr  12268  divgcdcoprmex  12270  cncongr1  12271  cncongr2  12272  prmexpb  12319  rpexp  12321  pythagtriplem1  12434  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem12  12444  pythagtriplem13  12445  pythagtriplem15  12447  pythagtriplem19  12451  pcdiv  12471  dvdsprmpweqle  12506  sumhashdc  12516  pcbc  12520  4sqlem12  12571  4sqlem18  12577  unennn  12614  nninfdc  12670  fvsetsid  12712  ressressg  12753  rngmulrg  12815  imasaddvallemg  12958  qusaddvallemg  12976  mgmsscl  13004  plusfvalg  13006  ress0g  13084  gsumfzz  13127  grpasscan2  13196  grpidrcan  13197  grpidlcan  13198  grpinvadd  13210  grppncan  13223  dfgrp3me  13232  grpsubpropd2  13237  imasgrp2  13240  imasgrp  13241  mhmmnd  13246  mulgnnsubcl  13264  mulgnn0subcl  13265  mulgsubcl  13266  mulgaddcomlem  13275  mulgaddcom  13276  mulgpropdg  13294  submmulg  13296  subgcl  13314  subgsubcl  13315  subgsub  13316  subgmulg  13318  nsgconj  13336  ghmsub  13381  ghmnsgima  13398  ghmeqker  13401  f1ghm0to0  13402  ablinvadd  13440  ablpncan2  13446  subgabl  13462  rngcl  13500  imasrng  13512  srgcl  13526  ringcl  13569  crngcom  13570  ringidss  13585  ringcom  13587  mulgass2  13614  imasring  13620  opprringbg  13636  unitmulcl  13669  unitmulclb  13670  dvrcl  13691  unitdvcl  13692  dvrcan1  13696  dvrcan3  13697  rhmmul  13720  subrngmcl  13765  subrgmcl  13789  subrgdv  13794  domneq0  13828  islmod  13847  scafvalg  13863  lmodcom  13889  lmodprop2d  13904  rmodislmodlem  13906  rmodislmod  13907  lsselg  13917  lssvnegcl  13932  lspss  13955  lspun  13958  lspsnvsi  13974  lsslsp  13985  sralmod  14006  lidlnegcl  14041  rspssp  14050  rnglidlrng  14054  qus2idrng  14081  zndvds  14205  basgen  14316  2basgeng  14318  ntrss  14355  neiss  14386  opnneiss  14394  restco  14410  restabs  14411  cnprcl2k  14442  cnpf2  14443  lmconst  14452  cnpnei  14455  cnptoprest  14475  cnmpt2t  14529  psmetsym  14565  psmetge0  14567  xmetge0  14601  xmetsym  14604  blvalps  14624  blval  14625  ssblps  14661  ssbl  14662  blpnfctr  14675  xmssym  14705  bdxmet  14737  metcnp3  14747  dvfvalap  14917  dvid  14931  dvidre  14933  dvcnp2cntop  14935  elplyr  14976  ply1term  14979  plypow  14980  ptolemy  15060  rpcxpadd  15141  rpcxpsub  15144  rpmulcxp  15145  cxpmul  15148  rpcxple2  15154  rpcxplt2  15155  cxpcom  15174  rplogbval  15181  rplogbcl  15182  rplogbchbase  15186  rplogbreexp  15189  relogbexpap  15194  logbleb  15197  logblt  15198  rplogbcxp  15199  rpcxplogb  15200  relogbcxpbap  15201  sgmppw  15228  lgslem1  15241  lgsfvalg  15246  lgsval4  15261  lgsneg  15265  lgsne0  15279  lgsdinn0  15289  lgsquad  15321