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  2941  sotri2  5064  sotri3  5065  feq123  5396  resasplitss  5434  sefvex  5576  ftpg  5743  fsnunf  5759  fnfvima  5794  cocan1  5831  cocan2  5832  f1oiso2  5871  riotass  5902  moriotass  5903  ovmpox  6048  ovmpoga  6049  fvmpopr2d  6056  caovimo  6114  ofrval  6143  dfsmo2  6342  tfr1onlembfn  6399  tfrcllembfn  6412  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecrdg  6463  nnsucsssuc  6547  f1oen2g  6811  f1dom2g  6812  xpdom3m  6890  mapxpen  6906  diffifi  6952  unfidisj  6980  undifdc  6982  ssfidc  6993  sbthlemi9  7026  ctssdc  7174  endjudisj  7272  djuassen  7279  xpdjuen  7280  mulcanenq  7447  ltanqg  7462  addnnnq0  7511  nnanq0  7520  prltlu  7549  distrprg  7650  ltexprlemm  7662  recexprlem1ssl  7695  recexprlem1ssu  7696  addsrpr  7807  mulsrpr  7808  mulasssrg  7820  recexgt0sr  7835  ltpsrprg  7865  axmulass  7935  axpre-ltadd  7948  ltxrlt  8087  subadd2  8225  addsubass  8231  nppcan  8243  nppcan3  8245  subcan2  8246  subsub2  8249  subsub4  8254  pnpcan  8260  pnncan  8262  subcan  8276  subdi  8406  ltadd1  8450  leadd1  8451  leadd2  8452  ltsubadd  8453  ltsubadd2  8454  lesubadd  8455  lesubadd2  8456  ltaddsub  8457  leaddsub  8459  lesub1  8477  lesub2  8478  ltsub1  8479  ltsub2  8480  ltaddsublt  8592  gt0add  8594  reapadd1  8617  remulext1  8620  remulext2  8621  apadd2  8630  mulext2  8634  mulap0r  8636  leltap  8646  ltap  8654  apsub1  8663  divap0b  8704  divmulasscomap  8717  divcanap5  8735  dmdcanap  8743  redivclap  8752  div2negap  8756  lt2msq1  8906  ltdiv2  8908  ofnegsub  8983  nndivtr  9026  difgtsumgt  9389  gtndiv  9415  eluzsub  9625  nn01to3  9685  qdivcl  9711  irrmul  9715  rpgecl  9751  divge1  9792  xaddass  9938  xltadd1  9945  ubioog  9983  ubioc1  9998  lbico1  9999  iccleub  10000  lbicc2  10053  ubicc2  10054  icoshftf1o  10060  fzen  10112  elfz1b  10159  uznfz  10172  elfzo0  10252  elfzo0z  10254  ubmelfzo  10270  fzonn0p1p1  10283  ubmelm1fzo  10296  qbtwnre  10328  flqwordi  10360  flltdivnn0lt  10376  ceiqle  10387  modqval  10398  modqvalr  10399  modqcl  10400  flqpmodeq  10401  modq0  10403  mulqmod0  10404  negqmod0  10405  modqge0  10406  modqlt  10407  modqdiffl  10409  modqdifz  10410  modqmulnn  10416  modqvalp1  10417  modqabs2  10432  modqmuladdnn0  10442  qnegmod  10443  addmodid  10446  modqeqmodmin  10468  modfzo0difsn  10469  addmodlteq  10472  frec2uzf1od  10480  expnegap0  10621  expgt1  10651  exprecap  10654  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  mulbinom2  10730  expnbnd  10737  fihashss  10890  fimaxq  10901  seq3coll  10916  shftfibg  10967  redivap  11021  imdivap  11028  cjdivap  11056  maxleast  11360  lemininf  11380  ltmininf  11381  bdtrilem  11385  bdtri  11386  xrmaxaddlem  11406  xrmaxadd  11407  xrmineqinf  11415  xrltmininf  11416  xrminltinf  11418  xrminadd  11421  climuni  11439  reccn2ap  11459  isumz  11535  fsumsplitsnun  11565  geoisum1c  11666  prodfap0  11691  prod1dc  11732  fprodabs  11762  cos12dec  11914  summodnegmod  11968  dvdsmultr2  11979  mulmoddvds  12008  divalglemeuneg  12067  zsupssdc  12094  gcdaddm  12124  gcdass  12155  mulgcd  12156  gcddiv  12159  nnminle  12175  lcmass  12226  mulgcddvds  12235  qredeq  12237  congr  12241  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  prmexpb  12292  rpexp  12294  pythagtriplem1  12406  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem12  12416  pythagtriplem13  12417  pythagtriplem15  12419  pythagtriplem19  12423  pcdiv  12443  dvdsprmpweqle  12478  sumhashdc  12488  pcbc  12492  4sqlem12  12543  4sqlem18  12549  unennn  12557  nninfdc  12613  fvsetsid  12655  ressressg  12696  rngmulrg  12758  imasaddvallemg  12901  qusaddvallemg  12919  mgmsscl  12947  plusfvalg  12949  ress0g  13027  gsumfzz  13070  grpasscan2  13139  grpidrcan  13140  grpidlcan  13141  grpinvadd  13153  grppncan  13166  dfgrp3me  13175  grpsubpropd2  13180  imasgrp2  13183  imasgrp  13184  mhmmnd  13189  mulgnnsubcl  13207  mulgnn0subcl  13208  mulgsubcl  13209  mulgaddcomlem  13218  mulgaddcom  13219  mulgpropdg  13237  submmulg  13239  subgcl  13257  subgsubcl  13258  subgsub  13259  subgmulg  13261  nsgconj  13279  ghmsub  13324  ghmnsgima  13341  ghmeqker  13344  f1ghm0to0  13345  ablinvadd  13383  ablpncan2  13389  subgabl  13405  rngcl  13443  imasrng  13455  srgcl  13469  ringcl  13512  crngcom  13513  ringidss  13528  ringcom  13530  mulgass2  13557  imasring  13563  opprringbg  13579  unitmulcl  13612  unitmulclb  13613  dvrcl  13634  unitdvcl  13635  dvrcan1  13639  dvrcan3  13640  rhmmul  13663  subrngmcl  13708  subrgmcl  13732  subrgdv  13737  domneq0  13771  islmod  13790  scafvalg  13806  lmodcom  13832  lmodprop2d  13847  rmodislmodlem  13849  rmodislmod  13850  lsselg  13860  lssvnegcl  13875  lspss  13898  lspun  13901  lspsnvsi  13917  lsslsp  13928  sralmod  13949  lidlnegcl  13984  rspssp  13993  rnglidlrng  13997  qus2idrng  14024  zndvds  14148  basgen  14259  2basgeng  14261  ntrss  14298  neiss  14329  opnneiss  14337  restco  14353  restabs  14354  cnprcl2k  14385  cnpf2  14386  lmconst  14395  cnpnei  14398  cnptoprest  14418  cnmpt2t  14472  psmetsym  14508  psmetge0  14510  xmetge0  14544  xmetsym  14547  blvalps  14567  blval  14568  ssblps  14604  ssbl  14605  blpnfctr  14618  xmssym  14648  bdxmet  14680  metcnp3  14690  dvfvalap  14860  dvid  14874  dvidre  14876  dvcnp2cntop  14878  elplyr  14919  ply1term  14922  plypow  14923  ptolemy  15000  rpcxpadd  15081  rpcxpsub  15084  rpmulcxp  15085  cxpmul  15088  rpcxple2  15093  rpcxplt2  15094  cxpcom  15112  rplogbval  15118  rplogbcl  15119  rplogbchbase  15123  rplogbreexp  15126  relogbexpap  15131  logbleb  15134  logblt  15135  rplogbcxp  15136  rpcxplogb  15137  relogbcxpbap  15138  lgslem1  15157  lgsfvalg  15162  lgsval4  15177  lgsneg  15181  lgsne0  15195  lgsdinn0  15205  lgsquad  15237