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  3000  sotri2  5165  sotri3  5166  feq123  5505  resasplitss  5549  fresaunres2disj  5550  sefvex  5696  ftpg  5873  fsnunf  5889  fnfvima  5926  cocan1  5966  cocan2  5967  f1oiso2  6006  riotass  6041  moriotass  6042  ovmpox  6190  ovmpoga  6191  fvmpopr2d  6198  caovimo  6256  ofrval  6286  suppvalfn  6454  fvn0elsuppb  6465  dfsmo2  6531  tfr1onlembfn  6588  tfrcllembfn  6601  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecrdg  6652  nnsucsssuc  6738  f1oen2g  7007  f1dom2g  7008  xpdom3m  7098  mapxpen  7114  diffifi  7164  unfidisj  7195  undifdc  7197  imaf1fi  7206  ssfidc  7211  sbthlemi9  7248  ctssdc  7417  endjudisj  7530  djuassen  7537  xpdjuen  7538  mulcanenq  7716  ltanqg  7731  addnnnq0  7780  nnanq0  7789  prltlu  7818  distrprg  7919  ltexprlemm  7931  recexprlem1ssl  7964  recexprlem1ssu  7965  addsrpr  8076  mulsrpr  8077  mulasssrg  8089  recexgt0sr  8104  ltpsrprg  8134  axmulass  8204  axpre-ltadd  8217  ltxrlt  8355  subadd2  8494  addsubass  8500  nppcan  8512  nppcan3  8514  subcan2  8515  subsub2  8518  subsub4  8523  pnpcan  8529  pnncan  8531  subcan  8545  subdi  8676  ltadd1  8721  leadd1  8722  leadd2  8723  ltsubadd  8724  ltsubadd2  8725  lesubadd  8726  lesubadd2  8727  ltaddsub  8728  leaddsub  8730  lesub1  8748  lesub2  8749  ltsub1  8750  ltsub2  8751  ltaddsublt  8863  gt0add  8865  reapadd1  8888  remulext1  8891  remulext2  8892  apadd2  8901  mulext2  8905  mulap0r  8907  leltap  8917  ltap  8925  apsub1  8934  divap0b  8977  divmulasscomap  8990  divcanap5  9008  dmdcanap  9016  redivclap  9025  div2negap  9029  lt2msq1  9179  ltdiv2  9181  ofnegsub  9256  nndivtr  9299  difgtsumgt  9667  zfidc  9676  gtndiv  9694  eluzsub  9905  nn01to3  9970  qdivcl  9996  irrmul  10000  rpgecl  10036  divge1  10077  xaddass  10224  xltadd1  10231  ubioog  10269  ubioc1  10284  lbico1  10285  iccleub  10286  lbicc2  10339  ubicc2  10340  icoshftf1o  10346  fzen  10400  elfz1b  10449  uznfz  10462  elfzo0  10545  elfzo0z  10548  ubmelfzo  10570  fzonn0p1p1  10583  ubmelm1fzo  10596  zsupssdc  10625  qbtwnre  10643  flqwordi  10675  flltdivnn0lt  10691  ceiqle  10702  modqval  10713  modqvalr  10714  modqcl  10715  flqpmodeq  10716  modq0  10718  mulqmod0  10719  negqmod0  10720  modqge0  10721  modqlt  10722  modqdiffl  10724  modqdifz  10725  modqmulnn  10731  modqvalp1  10732  modqabs2  10747  modqmuladdnn0  10757  qnegmod  10758  addmodid  10761  modqeqmodmin  10783  modfzo0difsn  10784  addmodlteq  10787  frec2uzf1od  10795  expnegap0  10936  expgt1  10966  exprecap  10969  expaddzaplem  10971  expaddzap  10972  expmulzap  10974  mulbinom2  11045  expnbnd  11053  fihashss  11209  fimaxq  11222  seq3coll  11242  ccatw2s1leng  11354  ccat2s1fvwd  11363  swrdval  11368  swrdnd  11379  swrdlen2  11382  pfxn0  11408  ccatopth2  11437  s3cl  11506  s3fv0g  11511  s3fv1g  11512  s3fv2g  11513  shftfibg  11533  redivap  11587  imdivap  11594  cjdivap  11622  maxleast  11926  lemininf  11947  ltmininf  11948  bdtrilem  11952  bdtri  11953  xrmaxaddlem  11973  xrmaxadd  11974  xrmineqinf  11982  xrltmininf  11983  xrminltinf  11985  xrminadd  11988  climuni  12006  reccn2ap  12026  isumz  12103  fsumsplitsnun  12133  geoisum1c  12234  prodfap0  12259  prod1dc  12300  fprodabs  12330  cos12dec  12482  summodnegmod  12536  dvdsmultr2  12547  mulmoddvds  12577  divalglemeuneg  12637  gcdaddm  12708  gcdass  12739  mulgcd  12740  gcddiv  12743  nnminle  12759  lcmass  12810  mulgcddvds  12819  qredeq  12821  congr  12825  divgcdcoprmex  12827  cncongr1  12828  cncongr2  12829  prmexpb  12876  rpexp  12878  pythagtriplem1  12991  pythagtriplem6  12996  pythagtriplem7  12997  pythagtriplem12  13001  pythagtriplem13  13002  pythagtriplem15  13004  pythagtriplem19  13008  pcdiv  13028  dvdsprmpweqle  13063  sumhashdc  13073  pcbc  13077  4sqlem12  13128  4sqlem18  13134  ballotfilemsgt1  13201  ballotfilemfrcn0  13220  unennn  13235  nninfdc  13291  fvsetsid  13333  ressressg  13375  rngmulrg  13438  imasaddvallemg  13582  qusaddvallemg  13600  mgmsscl  13627  plusfvalg  13629  ress0g  13707  imasmnd2  13710  imasmnd  13711  gsumfzz  13753  grpasscan2  13822  grpidrcan  13823  grpidlcan  13824  grpinvadd  13836  grppncan  13849  dfgrp3me  13858  grpsubpropd2  13863  imasgrp2  13866  imasgrp  13867  mhmmnd  13872  mulgnnsubcl  13890  mulgnn0subcl  13891  mulgsubcl  13892  mulgaddcomlem  13901  mulgaddcom  13902  mulgpropdg  13920  submmulg  13922  subgcl  13940  subgsubcl  13941  subgsub  13942  subgmulg  13944  nsgconj  13962  ghmsub  14007  ghmnsgima  14024  ghmeqker  14027  f1ghm0to0  14028  ablinvadd  14066  ablpncan2  14072  subgabl  14088  gfsumsn  14110  pwsinvg  14160  rngcl  14186  imasrng  14198  rng1zrlem  14201  srgcl  14216  ringcl  14259  crngcom  14260  ringidss  14275  ringcom  14277  mulgass2  14304  imasring  14310  opprringbg  14326  unitmulcl  14361  unitmulclb  14362  dvrcl  14383  unitdvcl  14384  dvrcan1  14388  dvrcan3  14389  rhmmul  14412  subrngmcl  14458  subrgmcl  14482  subrgdv  14487  domneq0  14522  islmod  14568  scafvalg  14584  lmodcom  14610  lmodprop2d  14625  rmodislmodlem  14627  rmodislmod  14628  lsselg  14638  lssvnegcl  14653  lspss  14676  lspun  14679  lspsnvsi  14695  lsslsp  14706  sralmod  14727  lidlnegcl  14762  rspssp  14771  rnglidlrng  14775  qus2idrng  14802  zndvds  14926  psrbagaddclfi  14954  psrbagcon  14955  basgen  15074  2basgeng  15076  ntrss  15113  neiss  15144  opnneiss  15152  restco  15168  restabs  15169  cnprcl2k  15200  cnpf2  15201  lmconst  15210  cnpnei  15213  cnptoprest  15233  cnmpt2t  15287  psmetsym  15323  psmetge0  15325  xmetge0  15359  xmetsym  15362  blvalps  15382  blval  15383  ssblps  15419  ssbl  15420  blpnfctr  15433  xmssym  15463  bdxmet  15495  metcnp3  15505  dvfvalap  15675  dvid  15689  dvidre  15691  dvcnp2cntop  15693  elplyr  15734  ply1term  15737  plypow  15738  ptolemy  15818  rpcxpadd  15899  rpcxpsub  15902  rpmulcxp  15903  cxpmul  15906  rpcxple2  15912  rpcxplt2  15913  cxpcom  15932  rplogbval  15939  rplogbcl  15940  rplogbchbase  15944  rplogbreexp  15947  relogbexpap  15952  logbleb  15955  logblt  15956  rplogbcxp  15957  rpcxplogb  15958  relogbcxpbap  15959  sgmppw  15989  lgslem1  16002  lgsfvalg  16007  lgsval4  16022  lgsneg  16026  lgsne0  16040  lgsdinn0  16050  lgsquad  16082  funvtxvalg  16160  funiedgvalg  16161  upgrex  16227  uhgr2edg  16330  usgr2v1e2w  16370  subumgredg2en  16395  iedginwlk  16481  upgrwlkedg  16485  clwwlkccat  16525  clwwlknonex2  16563  eulerpathprum  16604  dichmul0or  16643  repiecele0  16949  repiecege0  16950