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  2940  sotri2  5063  sotri3  5064  feq123  5395  resasplitss  5433  sefvex  5575  ftpg  5742  fsnunf  5758  fnfvima  5793  cocan1  5830  cocan2  5831  f1oiso2  5870  riotass  5901  moriotass  5902  ovmpox  6047  ovmpoga  6048  caovimo  6112  ofrval  6141  dfsmo2  6340  tfr1onlembfn  6397  tfrcllembfn  6410  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecrdg  6461  nnsucsssuc  6545  f1oen2g  6809  f1dom2g  6810  xpdom3m  6888  mapxpen  6904  diffifi  6950  unfidisj  6978  undifdc  6980  ssfidc  6991  sbthlemi9  7024  ctssdc  7172  endjudisj  7270  djuassen  7277  xpdjuen  7278  mulcanenq  7445  ltanqg  7460  addnnnq0  7509  nnanq0  7518  prltlu  7547  distrprg  7648  ltexprlemm  7660  recexprlem1ssl  7693  recexprlem1ssu  7694  addsrpr  7805  mulsrpr  7806  mulasssrg  7818  recexgt0sr  7833  ltpsrprg  7863  axmulass  7933  axpre-ltadd  7946  ltxrlt  8085  subadd2  8223  addsubass  8229  nppcan  8241  nppcan3  8243  subcan2  8244  subsub2  8247  subsub4  8252  pnpcan  8258  pnncan  8260  subcan  8274  subdi  8404  ltadd1  8448  leadd1  8449  leadd2  8450  ltsubadd  8451  ltsubadd2  8452  lesubadd  8453  lesubadd2  8454  ltaddsub  8455  leaddsub  8457  lesub1  8475  lesub2  8476  ltsub1  8477  ltsub2  8478  ltaddsublt  8590  gt0add  8592  reapadd1  8615  remulext1  8618  remulext2  8619  apadd2  8628  mulext2  8632  mulap0r  8634  leltap  8644  ltap  8652  apsub1  8661  divap0b  8702  divmulasscomap  8715  divcanap5  8733  dmdcanap  8741  redivclap  8750  div2negap  8754  lt2msq1  8904  ltdiv2  8906  ofnegsub  8981  nndivtr  9024  difgtsumgt  9386  gtndiv  9412  eluzsub  9622  nn01to3  9682  qdivcl  9708  irrmul  9712  rpgecl  9748  divge1  9789  xaddass  9935  xltadd1  9942  ubioog  9980  ubioc1  9995  lbico1  9996  iccleub  9997  lbicc2  10050  ubicc2  10051  icoshftf1o  10057  fzen  10109  elfz1b  10156  uznfz  10169  elfzo0  10249  elfzo0z  10251  ubmelfzo  10267  fzonn0p1p1  10280  ubmelm1fzo  10293  qbtwnre  10325  flqwordi  10357  flltdivnn0lt  10373  ceiqle  10384  modqval  10395  modqvalr  10396  modqcl  10397  flqpmodeq  10398  modq0  10400  mulqmod0  10401  negqmod0  10402  modqge0  10403  modqlt  10404  modqdiffl  10406  modqdifz  10407  modqmulnn  10413  modqvalp1  10414  modqabs2  10429  modqmuladdnn0  10439  qnegmod  10440  addmodid  10443  modqeqmodmin  10465  modfzo0difsn  10466  addmodlteq  10469  frec2uzf1od  10477  expnegap0  10618  expgt1  10648  exprecap  10651  expaddzaplem  10653  expaddzap  10654  expmulzap  10656  mulbinom2  10727  expnbnd  10734  fihashss  10887  fimaxq  10898  seq3coll  10913  shftfibg  10964  redivap  11018  imdivap  11025  cjdivap  11053  maxleast  11357  lemininf  11377  ltmininf  11378  bdtrilem  11382  bdtri  11383  xrmaxaddlem  11403  xrmaxadd  11404  xrmineqinf  11412  xrltmininf  11413  xrminltinf  11415  xrminadd  11418  climuni  11436  reccn2ap  11456  isumz  11532  fsumsplitsnun  11562  geoisum1c  11663  prodfap0  11688  prod1dc  11729  fprodabs  11759  cos12dec  11911  summodnegmod  11965  dvdsmultr2  11976  mulmoddvds  12005  divalglemeuneg  12064  zsupssdc  12091  gcdaddm  12121  gcdass  12152  mulgcd  12153  gcddiv  12156  nnminle  12172  lcmass  12223  mulgcddvds  12232  qredeq  12234  congr  12238  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  prmexpb  12289  rpexp  12291  pythagtriplem1  12403  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem12  12413  pythagtriplem13  12414  pythagtriplem15  12416  pythagtriplem19  12420  pcdiv  12440  dvdsprmpweqle  12475  sumhashdc  12485  pcbc  12489  4sqlem12  12540  4sqlem18  12546  unennn  12554  nninfdc  12610  fvsetsid  12652  ressressg  12693  rngmulrg  12755  imasaddvallemg  12898  qusaddvallemg  12916  mgmsscl  12944  plusfvalg  12946  ress0g  13024  gsumfzz  13067  grpasscan2  13136  grpidrcan  13137  grpidlcan  13138  grpinvadd  13150  grppncan  13163  dfgrp3me  13172  grpsubpropd2  13177  imasgrp2  13180  imasgrp  13181  mhmmnd  13186  mulgnnsubcl  13204  mulgnn0subcl  13205  mulgsubcl  13206  mulgaddcomlem  13215  mulgaddcom  13216  mulgpropdg  13234  submmulg  13236  subgcl  13254  subgsubcl  13255  subgsub  13256  subgmulg  13258  nsgconj  13276  ghmsub  13321  ghmnsgima  13338  ghmeqker  13341  f1ghm0to0  13342  ablinvadd  13380  ablpncan2  13386  subgabl  13402  rngcl  13440  imasrng  13452  srgcl  13466  ringcl  13509  crngcom  13510  ringidss  13525  ringcom  13527  mulgass2  13554  imasring  13560  opprringbg  13576  unitmulcl  13609  unitmulclb  13610  dvrcl  13631  unitdvcl  13632  dvrcan1  13636  dvrcan3  13637  rhmmul  13660  subrngmcl  13705  subrgmcl  13729  subrgdv  13734  domneq0  13768  islmod  13787  scafvalg  13803  lmodcom  13829  lmodprop2d  13844  rmodislmodlem  13846  rmodislmod  13847  lsselg  13857  lssvnegcl  13872  lspss  13895  lspun  13898  lspsnvsi  13914  lsslsp  13925  sralmod  13946  lidlnegcl  13981  rspssp  13990  rnglidlrng  13994  qus2idrng  14021  zndvds  14137  basgen  14248  2basgeng  14250  ntrss  14287  neiss  14318  opnneiss  14326  restco  14342  restabs  14343  cnprcl2k  14374  cnpf2  14375  lmconst  14384  cnpnei  14387  cnptoprest  14407  cnmpt2t  14461  psmetsym  14497  psmetge0  14499  xmetge0  14533  xmetsym  14536  blvalps  14556  blval  14557  ssblps  14593  ssbl  14594  blpnfctr  14607  xmssym  14637  bdxmet  14669  metcnp3  14679  dvfvalap  14835  dvid  14847  dvcnp2cntop  14848  elplyr  14886  ply1term  14889  plypow  14890  ptolemy  14959  rpcxpadd  15040  rpcxpsub  15043  rpmulcxp  15044  cxpmul  15047  rpcxple2  15052  rpcxplt2  15053  cxpcom  15071  rplogbval  15077  rplogbcl  15078  rplogbchbase  15082  rplogbreexp  15085  relogbexpap  15090  logbleb  15093  logblt  15094  rplogbcxp  15095  rpcxplogb  15096  relogbcxpbap  15097  lgslem1  15116  lgsfvalg  15121  lgsval4  15136  lgsneg  15140  lgsne0  15154  lgsdinn0  15164