Theorem simp3 1026

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simpl3  1029  simpr3  1032  simp3i  1035  simp3d  1038  simp13  1056  simp23  1059  simp33  1062  3anibar  1192  3ianorr  1346  intn3an3d  1395  stoic4a  1477  stoic4b  1478  mob2  2999  sotri2  5162  sotri3  5163  feq123  5502  resasplitss  5546  fresaunres2disj  5547  sefvex  5693  ftpg  5870  fsnunf  5886  fnfvima  5923  cocan1  5962  cocan2  5963  f1oiso2  6002  riotass  6035  moriotass  6036  ovmpox  6184  ovmpoga  6185  fvmpopr2d  6192  caovimo  6250  ofrval  6279  suppvalfn  6443  fvn0elsuppb  6454  dfsmo2  6520  tfr1onlembfn  6577  tfrcllembfn  6590  freccllem  6635  frecfcllem  6637  frecsuclem  6639  frecrdg  6641  nnsucsssuc  6727  f1oen2g  6996  f1dom2g  6997  xpdom3m  7087  mapxpen  7103  diffifi  7153  unfidisj  7184  undifdc  7186  imaf1fi  7195  ssfidc  7200  sbthlemi9  7237  ctssdc  7406  endjudisj  7519  djuassen  7526  xpdjuen  7527  mulcanenq  7705  ltanqg  7720  addnnnq0  7769  nnanq0  7778  prltlu  7807  distrprg  7908  ltexprlemm  7920  recexprlem1ssl  7953  recexprlem1ssu  7954  addsrpr  8065  mulsrpr  8066  mulasssrg  8078  recexgt0sr  8093  ltpsrprg  8123  axmulass  8193  axpre-ltadd  8206  ltxrlt  8344  subadd2  8482  addsubass  8488  nppcan  8500  nppcan3  8502  subcan2  8503  subsub2  8506  subsub4  8511  pnpcan  8517  pnncan  8519  subcan  8533  subdi  8663  ltadd1  8708  leadd1  8709  leadd2  8710  ltsubadd  8711  ltsubadd2  8712  lesubadd  8713  lesubadd2  8714  ltaddsub  8715  leaddsub  8717  lesub1  8735  lesub2  8736  ltsub1  8737  ltsub2  8738  ltaddsublt  8850  gt0add  8852  reapadd1  8875  remulext1  8878  remulext2  8879  apadd2  8888  mulext2  8892  mulap0r  8894  leltap  8904  ltap  8912  apsub1  8921  divap0b  8962  divmulasscomap  8975  divcanap5  8993  dmdcanap  9001  redivclap  9010  div2negap  9014  lt2msq1  9164  ltdiv2  9166  ofnegsub  9241  nndivtr  9284  difgtsumgt  9652  zfidc  9661  gtndiv  9679  eluzsub  9890  nn01to3  9955  qdivcl  9981  irrmul  9985  rpgecl  10021  divge1  10062  xaddass  10208  xltadd1  10215  ubioog  10253  ubioc1  10268  lbico1  10269  iccleub  10270  lbicc2  10323  ubicc2  10324  icoshftf1o  10330  fzen  10383  elfz1b  10431  uznfz  10444  elfzo0  10527  elfzo0z  10530  ubmelfzo  10552  fzonn0p1p1  10565  ubmelm1fzo  10578  zsupssdc  10605  qbtwnre  10623  flqwordi  10655  flltdivnn0lt  10671  ceiqle  10682  modqval  10693  modqvalr  10694  modqcl  10695  flqpmodeq  10696  modq0  10698  mulqmod0  10699  negqmod0  10700  modqge0  10701  modqlt  10702  modqdiffl  10704  modqdifz  10705  modqmulnn  10711  modqvalp1  10712  modqabs2  10727  modqmuladdnn0  10737  qnegmod  10738  addmodid  10741  modqeqmodmin  10763  modfzo0difsn  10764  addmodlteq  10767  frec2uzf1od  10775  expnegap0  10916  expgt1  10946  exprecap  10949  expaddzaplem  10951  expaddzap  10952  expmulzap  10954  mulbinom2  11025  expnbnd  11033  fihashss  11189  fimaxq  11202  seq3coll  11222  ccatw2s1leng  11334  ccat2s1fvwd  11343  swrdval  11348  swrdnd  11359  swrdlen2  11362  pfxn0  11388  ccatopth2  11417  s3cl  11486  s3fv0g  11491  s3fv1g  11492  s3fv2g  11493  shftfibg  11513  redivap  11567  imdivap  11574  cjdivap  11602  maxleast  11906  lemininf  11927  ltmininf  11928  bdtrilem  11932  bdtri  11933  xrmaxaddlem  11953  xrmaxadd  11954  xrmineqinf  11962  xrltmininf  11963  xrminltinf  11965  xrminadd  11968  climuni  11986  reccn2ap  12006  isumz  12083  fsumsplitsnun  12113  geoisum1c  12214  prodfap0  12239  prod1dc  12280  fprodabs  12310  cos12dec  12462  summodnegmod  12516  dvdsmultr2  12527  mulmoddvds  12557  divalglemeuneg  12617  gcdaddm  12688  gcdass  12719  mulgcd  12720  gcddiv  12723  nnminle  12739  lcmass  12790  mulgcddvds  12799  qredeq  12801  congr  12805  divgcdcoprmex  12807  cncongr1  12808  cncongr2  12809  prmexpb  12856  rpexp  12858  pythagtriplem1  12971  pythagtriplem6  12976  pythagtriplem7  12977  pythagtriplem12  12981  pythagtriplem13  12982  pythagtriplem15  12984  pythagtriplem19  12988  pcdiv  13008  dvdsprmpweqle  13043  sumhashdc  13053  pcbc  13057  4sqlem12  13108  4sqlem18  13114  unennn  13169  nninfdc  13225  fvsetsid  13267  ressressg  13309  rngmulrg  13372  imasaddvallemg  13549  qusaddvallemg  13567  mgmsscl  13595  plusfvalg  13597  ress0g  13677  imasmnd2  13686  imasmnd  13687  gsumfzz  13729  grpasscan2  13798  grpidrcan  13799  grpidlcan  13800  grpinvadd  13812  grppncan  13825  dfgrp3me  13834  grpsubpropd2  13839  pwsinvg  13846  imasgrp2  13848  imasgrp  13849  mhmmnd  13854  mulgnnsubcl  13872  mulgnn0subcl  13873  mulgsubcl  13874  mulgaddcomlem  13883  mulgaddcom  13884  mulgpropdg  13902  submmulg  13904  subgcl  13922  subgsubcl  13923  subgsub  13924  subgmulg  13926  nsgconj  13944  ghmsub  13989  ghmnsgima  14006  ghmeqker  14009  f1ghm0to0  14010  ablinvadd  14048  ablpncan2  14054  subgabl  14070  rngcl  14109  imasrng  14121  srgcl  14135  ringcl  14178  crngcom  14179  ringidss  14194  ringcom  14196  mulgass2  14223  imasring  14229  opprringbg  14245  unitmulcl  14280  unitmulclb  14281  dvrcl  14302  unitdvcl  14303  dvrcan1  14307  dvrcan3  14308  rhmmul  14331  subrngmcl  14377  subrgmcl  14401  subrgdv  14406  domneq0  14441  islmod  14488  scafvalg  14504  lmodcom  14530  lmodprop2d  14545  rmodislmodlem  14547  rmodislmod  14548  lsselg  14558  lssvnegcl  14573  lspss  14596  lspun  14599  lspsnvsi  14615  lsslsp  14626  sralmod  14647  lidlnegcl  14682  rspssp  14691  rnglidlrng  14695  qus2idrng  14722  zndvds  14846  psrbagaddclfi  14874  psrbagcon  14875  basgen  14994  2basgeng  14996  ntrss  15033  neiss  15064  opnneiss  15072  restco  15088  restabs  15089  cnprcl2k  15120  cnpf2  15121  lmconst  15130  cnpnei  15133  cnptoprest  15153  cnmpt2t  15207  psmetsym  15243  psmetge0  15245  xmetge0  15279  xmetsym  15282  blvalps  15302  blval  15303  ssblps  15339  ssbl  15340  blpnfctr  15353  xmssym  15383  bdxmet  15415  metcnp3  15425  dvfvalap  15595  dvid  15609  dvidre  15611  dvcnp2cntop  15613  elplyr  15654  ply1term  15657  plypow  15658  ptolemy  15738  rpcxpadd  15819  rpcxpsub  15822  rpmulcxp  15823  cxpmul  15826  rpcxple2  15832  rpcxplt2  15833  cxpcom  15852  rplogbval  15859  rplogbcl  15860  rplogbchbase  15864  rplogbreexp  15867  relogbexpap  15872  logbleb  15875  logblt  15876  rplogbcxp  15877  rpcxplogb  15878  relogbcxpbap  15879  sgmppw  15909  lgslem1  15922  lgsfvalg  15927  lgsval4  15942  lgsneg  15946  lgsne0  15960  lgsdinn0  15970  lgsquad  16002  funvtxvalg  16080  funiedgvalg  16081  upgrex  16147  uhgr2edg  16250  usgr2v1e2w  16290  subumgredg2en  16315  iedginwlk  16401  upgrwlkedg  16405  clwwlkccat  16445  clwwlknonex2  16483  eulerpathprum  16524  repiecele0  16859  repiecege0  16860  gfsumsn  16916