Theorem simp3 1025

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simpl3  1028  simpr3  1031  simp3i  1034  simp3d  1037  simp13  1055  simp23  1058  simp33  1061  3anibar  1191  3ianorr  1345  intn3an3d  1394  stoic4a  1476  stoic4b  1477  mob2  2986  sotri2  5134  sotri3  5135  feq123  5474  resasplitss  5516  sefvex  5660  ftpg  5838  fsnunf  5854  fnfvima  5889  cocan1  5928  cocan2  5929  f1oiso2  5968  riotass  6001  moriotass  6002  ovmpox  6150  ovmpoga  6151  fvmpopr2d  6158  caovimo  6216  ofrval  6246  dfsmo2  6453  tfr1onlembfn  6510  tfrcllembfn  6523  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecrdg  6574  nnsucsssuc  6660  f1oen2g  6928  f1dom2g  6929  xpdom3m  7018  mapxpen  7034  diffifi  7083  unfidisj  7114  undifdc  7116  imaf1fi  7125  ssfidc  7130  sbthlemi9  7164  ctssdc  7312  endjudisj  7425  djuassen  7432  xpdjuen  7433  mulcanenq  7605  ltanqg  7620  addnnnq0  7669  nnanq0  7678  prltlu  7707  distrprg  7808  ltexprlemm  7820  recexprlem1ssl  7853  recexprlem1ssu  7854  addsrpr  7965  mulsrpr  7966  mulasssrg  7978  recexgt0sr  7993  ltpsrprg  8023  axmulass  8093  axpre-ltadd  8106  ltxrlt  8245  subadd2  8383  addsubass  8389  nppcan  8401  nppcan3  8403  subcan2  8404  subsub2  8407  subsub4  8412  pnpcan  8418  pnncan  8420  subcan  8434  subdi  8564  ltadd1  8609  leadd1  8610  leadd2  8611  ltsubadd  8612  ltsubadd2  8613  lesubadd  8614  lesubadd2  8615  ltaddsub  8616  leaddsub  8618  lesub1  8636  lesub2  8637  ltsub1  8638  ltsub2  8639  ltaddsublt  8751  gt0add  8753  reapadd1  8776  remulext1  8779  remulext2  8780  apadd2  8789  mulext2  8793  mulap0r  8795  leltap  8805  ltap  8813  apsub1  8822  divap0b  8863  divmulasscomap  8876  divcanap5  8894  dmdcanap  8902  redivclap  8911  div2negap  8915  lt2msq1  9065  ltdiv2  9067  ofnegsub  9142  nndivtr  9185  difgtsumgt  9549  gtndiv  9575  eluzsub  9786  nn01to3  9851  qdivcl  9877  irrmul  9881  rpgecl  9917  divge1  9958  xaddass  10104  xltadd1  10111  ubioog  10149  ubioc1  10164  lbico1  10165  iccleub  10166  lbicc2  10219  ubicc2  10220  icoshftf1o  10226  fzen  10278  elfz1b  10325  uznfz  10338  elfzo0  10421  elfzo0z  10424  ubmelfzo  10446  fzonn0p1p1  10459  ubmelm1fzo  10472  zsupssdc  10499  qbtwnre  10517  flqwordi  10549  flltdivnn0lt  10565  ceiqle  10576  modqval  10587  modqvalr  10588  modqcl  10589  flqpmodeq  10590  modq0  10592  mulqmod0  10593  negqmod0  10594  modqge0  10595  modqlt  10596  modqdiffl  10598  modqdifz  10599  modqmulnn  10605  modqvalp1  10606  modqabs2  10621  modqmuladdnn0  10631  qnegmod  10632  addmodid  10635  modqeqmodmin  10657  modfzo0difsn  10658  addmodlteq  10661  frec2uzf1od  10669  expnegap0  10810  expgt1  10840  exprecap  10843  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  mulbinom2  10919  expnbnd  10926  fihashss  11081  fimaxq  11092  seq3coll  11107  ccatw2s1leng  11216  ccat2s1fvwd  11225  swrdval  11230  swrdnd  11241  swrdlen2  11244  pfxn0  11270  ccatopth2  11299  s3cl  11368  s3fv0g  11373  s3fv1g  11374  s3fv2g  11375  shftfibg  11382  redivap  11436  imdivap  11443  cjdivap  11471  maxleast  11775  lemininf  11796  ltmininf  11797  bdtrilem  11801  bdtri  11802  xrmaxaddlem  11822  xrmaxadd  11823  xrmineqinf  11831  xrltmininf  11832  xrminltinf  11834  xrminadd  11837  climuni  11855  reccn2ap  11875  isumz  11952  fsumsplitsnun  11982  geoisum1c  12083  prodfap0  12108  prod1dc  12149  fprodabs  12179  cos12dec  12331  summodnegmod  12385  dvdsmultr2  12396  mulmoddvds  12426  divalglemeuneg  12486  gcdaddm  12557  gcdass  12588  mulgcd  12589  gcddiv  12592  nnminle  12608  lcmass  12659  mulgcddvds  12668  qredeq  12670  congr  12674  divgcdcoprmex  12676  cncongr1  12677  cncongr2  12678  prmexpb  12725  rpexp  12727  pythagtriplem1  12840  pythagtriplem6  12845  pythagtriplem7  12846  pythagtriplem12  12850  pythagtriplem13  12851  pythagtriplem15  12853  pythagtriplem19  12857  pcdiv  12877  dvdsprmpweqle  12912  sumhashdc  12922  pcbc  12926  4sqlem12  12977  4sqlem18  12983  unennn  13020  nninfdc  13076  fvsetsid  13118  ressressg  13160  rngmulrg  13223  imasaddvallemg  13400  qusaddvallemg  13418  mgmsscl  13446  plusfvalg  13448  ress0g  13528  imasmnd2  13537  imasmnd  13538  gsumfzz  13580  grpasscan2  13649  grpidrcan  13650  grpidlcan  13651  grpinvadd  13663  grppncan  13676  dfgrp3me  13685  grpsubpropd2  13690  pwsinvg  13697  imasgrp2  13699  imasgrp  13700  mhmmnd  13705  mulgnnsubcl  13723  mulgnn0subcl  13724  mulgsubcl  13725  mulgaddcomlem  13734  mulgaddcom  13735  mulgpropdg  13753  submmulg  13755  subgcl  13773  subgsubcl  13774  subgsub  13775  subgmulg  13777  nsgconj  13795  ghmsub  13840  ghmnsgima  13857  ghmeqker  13860  f1ghm0to0  13861  ablinvadd  13899  ablpncan2  13905  subgabl  13921  rngcl  13960  imasrng  13972  srgcl  13986  ringcl  14029  crngcom  14030  ringidss  14045  ringcom  14047  mulgass2  14074  imasring  14080  opprringbg  14096  unitmulcl  14130  unitmulclb  14131  dvrcl  14152  unitdvcl  14153  dvrcan1  14157  dvrcan3  14158  rhmmul  14181  subrngmcl  14226  subrgmcl  14250  subrgdv  14255  domneq0  14289  islmod  14308  scafvalg  14324  lmodcom  14350  lmodprop2d  14365  rmodislmodlem  14367  rmodislmod  14368  lsselg  14378  lssvnegcl  14393  lspss  14416  lspun  14419  lspsnvsi  14435  lsslsp  14446  sralmod  14467  lidlnegcl  14502  rspssp  14511  rnglidlrng  14515  qus2idrng  14542  zndvds  14666  basgen  14807  2basgeng  14809  ntrss  14846  neiss  14877  opnneiss  14885  restco  14901  restabs  14902  cnprcl2k  14933  cnpf2  14934  lmconst  14943  cnpnei  14946  cnptoprest  14966  cnmpt2t  15020  psmetsym  15056  psmetge0  15058  xmetge0  15092  xmetsym  15095  blvalps  15115  blval  15116  ssblps  15152  ssbl  15153  blpnfctr  15166  xmssym  15196  bdxmet  15228  metcnp3  15238  dvfvalap  15408  dvid  15422  dvidre  15424  dvcnp2cntop  15426  elplyr  15467  ply1term  15470  plypow  15471  ptolemy  15551  rpcxpadd  15632  rpcxpsub  15635  rpmulcxp  15636  cxpmul  15639  rpcxple2  15645  rpcxplt2  15646  cxpcom  15665  rplogbval  15672  rplogbcl  15673  rplogbchbase  15677  rplogbreexp  15680  relogbexpap  15685  logbleb  15688  logblt  15689  rplogbcxp  15690  rpcxplogb  15691  relogbcxpbap  15692  sgmppw  15719  lgslem1  15732  lgsfvalg  15737  lgsval4  15752  lgsneg  15756  lgsne0  15770  lgsdinn0  15780  lgsquad  15812  funvtxvalg  15890  funiedgvalg  15891  upgrex  15957  uhgr2edg  16060  usgr2v1e2w  16100  subumgredg2en  16125  iedginwlk  16211  upgrwlkedg  16215  clwwlkccat  16255  clwwlknonex2  16293  gfsumsn  16706