Theorem simp3 1030

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl3  1033  simpr3  1036  simp3i  1039  simp3d  1042  simp13  1060  simp23  1063  simp33  1066  3anibar  1196  3ianorr  1350  intn3an3d  1399  stoic4a  1481  stoic4b  1482  mob2  3006  ifprdc  3819  sotri2  5188  sotri3  5189  feq123  5528  resasplitss  5572  fresaunres2disj  5573  sefvex  5719  ftpg  5902  fsnunf  5918  fnfvima  5956  cocan1  5996  cocan2  5997  f1oiso2  6036  riotass  6071  moriotass  6072  ovmpox  6220  ovmpoga  6221  fvmpopr2d  6228  caovimo  6286  ofrval  6317  suppvalfn  6485  fvn0elsuppb  6496  dfsmo2  6562  tfr1onlembfn  6619  tfrcllembfn  6632  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecrdg  6683  nnsucsssuc  6769  mapm  6974  f1oen2g  7046  f1dom2g  7047  xpdom3m  7137  mapxpen  7153  diffifi  7203  unfidisj  7234  undifdc  7236  imaf1fi  7245  ssfidc  7250  sbthlemi9  7288  fdcf1  7322  ctssdc  7460  endjudisj  7573  djuassen  7580  xpdjuen  7581  mulcanenq  7759  ltanqg  7774  addnnnq0  7823  nnanq0  7832  prltlu  7861  distrprg  7962  ltexprlemm  7974  recexprlem1ssl  8007  recexprlem1ssu  8008  addsrpr  8119  mulsrpr  8120  mulasssrg  8132  recexgt0sr  8147  ltpsrprg  8177  axmulass  8247  axpre-ltadd  8260  ltxrlt  8398  subadd2  8538  addsubass  8544  nppcan  8556  nppcan3  8558  subcan2  8559  subsub2  8562  subsub4  8567  pnpcan  8573  pnncan  8575  subcan  8589  subdi  8720  ltadd1  8765  leadd1  8766  leadd2  8767  ltsubadd  8768  ltsubadd2  8769  lesubadd  8770  lesubadd2  8771  ltaddsub  8772  leaddsub  8774  lesub1  8792  lesub2  8793  ltsub1  8794  ltsub2  8795  ltaddsublt  8908  gt0add  8910  reapadd1  8933  remulext1  8936  remulext2  8937  apadd2  8946  mulext2  8950  mulap0r  8952  leltap  8962  ltap  8970  apsub1  8979  divap0b  9022  divmulasscomap  9035  divcanap5  9053  dmdcanap  9061  redivclap  9070  div2negap  9074  lt2msq1  9224  ltdiv2  9226  ofsubeq0  9301  ofnegsub  9302  indfval  9309  ind1  9310  nndivtr  9356  difgtsumgt  9726  zfidc  9735  gtndiv  9753  eluzsub  9969  nn01to3  10034  qdivcl  10060  irrmul  10065  rpgecl  10101  divge1  10142  xaddass  10289  xltadd1  10296  ubioog  10334  ubioc1  10349  lbico1  10350  iccleub  10351  lbicc2  10404  ubicc2  10405  icoshftf1o  10411  fzen  10465  elfz1b  10515  uznfz  10528  elfzo0  10611  elfzo0z  10614  ubmelfzo  10636  fzonn0p1p1  10649  ubmelm1fzo  10662  zsupssdc  10691  qbtwnre  10709  flqwordi  10745  flltdivnn0lt  10761  ceiqle  10772  modqval  10783  modqvalr  10784  modqcl  10785  flqpmodeq  10786  modq0  10788  mulqmod0  10789  negqmod0  10790  modqge0  10791  modqlt  10792  modqdiffl  10794  modqdifz  10795  modqmulnn  10801  modqvalp1  10802  modqabs2  10817  modqmuladdnn0  10827  qnegmod  10828  addmodid  10831  modqeqmodmin  10853  modfzo0difsn  10854  addmodlteq  10857  frec2uzf1od  10865  expnegap0  11006  expgt1  11036  exprecap  11039  expaddzaplem  11041  expaddzap  11042  expmulzap  11044  mulbinom2  11115  expnbnd  11123  fihashss  11280  fimaxq  11293  seq3coll  11317  ccatw2s1leng  11429  ccat2s1fvwd  11438  swrdval  11443  swrdnd  11454  swrdlen2  11457  pfxn0  11483  ccatopth2  11512  s3cl  11581  s3fv0g  11586  s3fv1g  11587  s3fv2g  11588  shftfibg  11608  redivap  11662  imdivap  11669  cjdivap  11698  maxleast  12003  lemininf  12025  ltmininf  12026  bdtrilem  12031  bdtri  12032  xrmaxaddlem  12052  xrmaxadd  12053  xrmineqinf  12061  xrltmininf  12062  xrminltinf  12064  xrminadd  12067  climuni  12085  reccn2ap  12105  isumz  12182  fsumsplitsnun  12212  geoisum1c  12313  prodfap0  12338  prod1dc  12379  fprodabs  12409  cos12dec  12561  summodnegmod  12615  dvdsmultr2  12626  mulmoddvds  12656  divalglemeuneg  12716  gcdaddm  12787  gcdass  12818  mulgcd  12819  gcddiv  12822  nnminle  12838  lcmass  12889  mulgcddvds  12898  qredeq  12900  congr  12904  divgcdcoprmex  12906  cncongr1  12907  cncongr2  12908  prmexpb  12956  rpexp  12958  pythagtriplem1  13074  pythagtriplem6  13079  pythagtriplem7  13080  pythagtriplem12  13084  pythagtriplem13  13085  pythagtriplem15  13087  pythagtriplem19  13091  pcdiv  13111  dvdsprmpweqle  13146  sumhashdc  13156  pcbc  13160  4sqlem12  13211  4sqlem18  13217  ballotfilemsgt1  13313  ballotfilemfrcn0  13332  unennn  13347  nninfdc  13403  fvsetsid  13445  ressressg  13489  rngmulrg  13552  imasaddvallemg  13696  qusaddvallemg  13714  mgmsscl  13741  plusfvalg  13743  ress0g  13816  imasmnd2  13819  imasmnd  13820  grpasscan2  13929  grpidrcan  13930  grpidlcan  13931  grpinvadd  13943  grppncan  13956  dfgrp3me  13965  grpsubpropd2  13970  imasgrp2  13973  imasgrp  13974  mhmmnd  13979  mulgnnsubcl  13997  mulgnn0subcl  13998  mulgsubcl  13999  mulgaddcomlem  14008  mulgaddcom  14009  mulgpropdg  14027  submmulg  14029  subgcl  14047  subgsubcl  14048  subgsub  14049  subgmulg  14051  nsgconj  14069  ghmsub  14114  ghmnsgima  14131  ghmeqker  14134  f1ghm0to0  14135  ablinvadd  14205  ablpncan2  14211  subgabl  14227  gsumsncmn  14247  gsumconstcmn  14267  pwsinvg  14323  rngcl  14351  imasrng  14363  rng1zrlem  14366  srgcl  14382  ringcl  14425  crngcom  14426  ringidss  14442  ringcom  14444  mulgass2  14471  imasring  14479  opprringbg  14495  unitmulcl  14530  unitmulclb  14531  dvrcl  14552  unitdvcl  14553  dvrcan1  14557  dvrcan3  14558  rhmmul  14581  subrngmcl  14627  subrgmcl  14651  subrgdv  14656  domneq0  14691  islmod  14737  scafvalg  14754  lmodcom  14780  lmodprop2d  14795  rmodislmodlem  14797  rmodislmod  14798  lsselg  14808  lssvnegcl  14823  lspss  14846  lspun  14849  lspsnvsi  14865  lsslsp  14876  sralmod  14897  lidlnegcl  14932  rspssp  14941  rnglidlrng  14945  qus2idrng  14972  zndvds  15094  aspss  15129  asclmul1  15139  asclmul2  15140  ascldimul  15141  asclinvg  15142  asclmulg  15154  psrbagdceq  15169  psrbagaddclfi  15175  psrbagcon  15176  psrringfi  15209  mvrf1fi  15215  basgen  15318  2basgeng  15320  ntrss  15357  neiss  15388  opnneiss  15396  restco  15412  restabs  15413  cnprcl2k  15444  cnpf2  15445  lmconst  15454  cnpnei  15457  cnptoprest  15477  cnmpt2t  15531  psmetsym  15567  psmetge0  15569  xmetge0  15603  xmetsym  15606  blvalps  15626  blval  15627  ssblps  15663  ssbl  15664  blpnfctr  15677  xmssym  15707  bdxmet  15739  metcnp3  15749  dvfvalap  15919  dvid  15933  dvidre  15935  dvcnp2cntop  15937  elplyr  15978  ply1term  15981  plypow  15982  ptolemy  16063  logfac  16138  rpcxpadd  16150  rpcxpsub  16153  rpmulcxp  16154  cxpmul  16157  rpcxple2  16165  rpcxplt2  16166  cxpcom  16185  efnthr  16188  rplogbval  16193  rplogbcl  16194  rplogbchbase  16198  rplogbreexp  16201  relogbexpap  16206  logbleb  16209  logblt  16210  rplogbcxp  16211  rpcxplogb  16212  relogbcxpbap  16213  chtqwordi  16275  ppiqwordi  16280  sgmppw  16298  bcmono  16316  prmefexple  16320  lgslem1  16336  lgsfvalg  16341  lgsval4  16356  lgsneg  16360  lgsne0  16374  lgsdinn0  16384  lgsquad  16416  funvtxvalg  16494  funiedgvalg  16495  upgrex  16561  uhgr2edg  16664  usgr2v1e2w  16704  subumgredg2en  16729  iedginwlk  16815  upgrwlkedg  16819  clwwlkccat  16859  clwwlknonex2  16897  eulerpathprum  16938  dichmul0or  16977  repiecele0  17293  repiecege0  17294