Theorem simp3 1023

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  simpl3  1026  simpr3  1029  simp3i  1032  simp3d  1035  simp13  1053  simp23  1056  simp33  1059  3anibar  1189  3ianorr  1343  intn3an3d  1392  stoic4a  1474  stoic4b  1475  mob2  2984  sotri2  5132  sotri3  5133  feq123  5471  resasplitss  5513  sefvex  5656  ftpg  5833  fsnunf  5849  fnfvima  5884  cocan1  5923  cocan2  5924  f1oiso2  5963  riotass  5996  moriotass  5997  ovmpox  6145  ovmpoga  6146  fvmpopr2d  6153  caovimo  6211  ofrval  6241  dfsmo2  6448  tfr1onlembfn  6505  tfrcllembfn  6518  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecrdg  6569  nnsucsssuc  6655  f1oen2g  6923  f1dom2g  6924  xpdom3m  7013  mapxpen  7029  diffifi  7078  unfidisj  7109  undifdc  7111  ssfidc  7124  sbthlemi9  7158  ctssdc  7306  endjudisj  7418  djuassen  7425  xpdjuen  7426  mulcanenq  7598  ltanqg  7613  addnnnq0  7662  nnanq0  7671  prltlu  7700  distrprg  7801  ltexprlemm  7813  recexprlem1ssl  7846  recexprlem1ssu  7847  addsrpr  7958  mulsrpr  7959  mulasssrg  7971  recexgt0sr  7986  ltpsrprg  8016  axmulass  8086  axpre-ltadd  8099  ltxrlt  8238  subadd2  8376  addsubass  8382  nppcan  8394  nppcan3  8396  subcan2  8397  subsub2  8400  subsub4  8405  pnpcan  8411  pnncan  8413  subcan  8427  subdi  8557  ltadd1  8602  leadd1  8603  leadd2  8604  ltsubadd  8605  ltsubadd2  8606  lesubadd  8607  lesubadd2  8608  ltaddsub  8609  leaddsub  8611  lesub1  8629  lesub2  8630  ltsub1  8631  ltsub2  8632  ltaddsublt  8744  gt0add  8746  reapadd1  8769  remulext1  8772  remulext2  8773  apadd2  8782  mulext2  8786  mulap0r  8788  leltap  8798  ltap  8806  apsub1  8815  divap0b  8856  divmulasscomap  8869  divcanap5  8887  dmdcanap  8895  redivclap  8904  div2negap  8908  lt2msq1  9058  ltdiv2  9060  ofnegsub  9135  nndivtr  9178  difgtsumgt  9542  gtndiv  9568  eluzsub  9779  nn01to3  9844  qdivcl  9870  irrmul  9874  rpgecl  9910  divge1  9951  xaddass  10097  xltadd1  10104  ubioog  10142  ubioc1  10157  lbico1  10158  iccleub  10159  lbicc2  10212  ubicc2  10213  icoshftf1o  10219  fzen  10271  elfz1b  10318  uznfz  10331  elfzo0  10414  elfzo0z  10416  ubmelfzo  10438  fzonn0p1p1  10451  ubmelm1fzo  10464  zsupssdc  10491  qbtwnre  10509  flqwordi  10541  flltdivnn0lt  10557  ceiqle  10568  modqval  10579  modqvalr  10580  modqcl  10581  flqpmodeq  10582  modq0  10584  mulqmod0  10585  negqmod0  10586  modqge0  10587  modqlt  10588  modqdiffl  10590  modqdifz  10591  modqmulnn  10597  modqvalp1  10598  modqabs2  10613  modqmuladdnn0  10623  qnegmod  10624  addmodid  10627  modqeqmodmin  10649  modfzo0difsn  10650  addmodlteq  10653  frec2uzf1od  10661  expnegap0  10802  expgt1  10832  exprecap  10835  expaddzaplem  10837  expaddzap  10838  expmulzap  10840  mulbinom2  10911  expnbnd  10918  fihashss  11073  fimaxq  11084  seq3coll  11099  ccatw2s1leng  11208  ccat2s1fvwd  11217  swrdval  11222  swrdnd  11233  swrdlen2  11236  pfxn0  11262  ccatopth2  11291  s3cl  11360  s3fv0g  11365  s3fv1g  11366  s3fv2g  11367  shftfibg  11374  redivap  11428  imdivap  11435  cjdivap  11463  maxleast  11767  lemininf  11788  ltmininf  11789  bdtrilem  11793  bdtri  11794  xrmaxaddlem  11814  xrmaxadd  11815  xrmineqinf  11823  xrltmininf  11824  xrminltinf  11826  xrminadd  11829  climuni  11847  reccn2ap  11867  isumz  11943  fsumsplitsnun  11973  geoisum1c  12074  prodfap0  12099  prod1dc  12140  fprodabs  12170  cos12dec  12322  summodnegmod  12376  dvdsmultr2  12387  mulmoddvds  12417  divalglemeuneg  12477  gcdaddm  12548  gcdass  12579  mulgcd  12580  gcddiv  12583  nnminle  12599  lcmass  12650  mulgcddvds  12659  qredeq  12661  congr  12665  divgcdcoprmex  12667  cncongr1  12668  cncongr2  12669  prmexpb  12716  rpexp  12718  pythagtriplem1  12831  pythagtriplem6  12836  pythagtriplem7  12837  pythagtriplem12  12841  pythagtriplem13  12842  pythagtriplem15  12844  pythagtriplem19  12848  pcdiv  12868  dvdsprmpweqle  12903  sumhashdc  12913  pcbc  12917  4sqlem12  12968  4sqlem18  12974  unennn  13011  nninfdc  13067  fvsetsid  13109  ressressg  13151  rngmulrg  13214  imasaddvallemg  13391  qusaddvallemg  13409  mgmsscl  13437  plusfvalg  13439  ress0g  13519  imasmnd2  13528  imasmnd  13529  gsumfzz  13571  grpasscan2  13640  grpidrcan  13641  grpidlcan  13642  grpinvadd  13654  grppncan  13667  dfgrp3me  13676  grpsubpropd2  13681  pwsinvg  13688  imasgrp2  13690  imasgrp  13691  mhmmnd  13696  mulgnnsubcl  13714  mulgnn0subcl  13715  mulgsubcl  13716  mulgaddcomlem  13725  mulgaddcom  13726  mulgpropdg  13744  submmulg  13746  subgcl  13764  subgsubcl  13765  subgsub  13766  subgmulg  13768  nsgconj  13786  ghmsub  13831  ghmnsgima  13848  ghmeqker  13851  f1ghm0to0  13852  ablinvadd  13890  ablpncan2  13896  subgabl  13912  rngcl  13950  imasrng  13962  srgcl  13976  ringcl  14019  crngcom  14020  ringidss  14035  ringcom  14037  mulgass2  14064  imasring  14070  opprringbg  14086  unitmulcl  14120  unitmulclb  14121  dvrcl  14142  unitdvcl  14143  dvrcan1  14147  dvrcan3  14148  rhmmul  14171  subrngmcl  14216  subrgmcl  14240  subrgdv  14245  domneq0  14279  islmod  14298  scafvalg  14314  lmodcom  14340  lmodprop2d  14355  rmodislmodlem  14357  rmodislmod  14358  lsselg  14368  lssvnegcl  14383  lspss  14406  lspun  14409  lspsnvsi  14425  lsslsp  14436  sralmod  14457  lidlnegcl  14492  rspssp  14501  rnglidlrng  14505  qus2idrng  14532  zndvds  14656  basgen  14797  2basgeng  14799  ntrss  14836  neiss  14867  opnneiss  14875  restco  14891  restabs  14892  cnprcl2k  14923  cnpf2  14924  lmconst  14933  cnpnei  14936  cnptoprest  14956  cnmpt2t  15010  psmetsym  15046  psmetge0  15048  xmetge0  15082  xmetsym  15085  blvalps  15105  blval  15106  ssblps  15142  ssbl  15143  blpnfctr  15156  xmssym  15186  bdxmet  15218  metcnp3  15228  dvfvalap  15398  dvid  15412  dvidre  15414  dvcnp2cntop  15416  elplyr  15457  ply1term  15460  plypow  15461  ptolemy  15541  rpcxpadd  15622  rpcxpsub  15625  rpmulcxp  15626  cxpmul  15629  rpcxple2  15635  rpcxplt2  15636  cxpcom  15655  rplogbval  15662  rplogbcl  15663  rplogbchbase  15667  rplogbreexp  15670  relogbexpap  15675  logbleb  15678  logblt  15679  rplogbcxp  15680  rpcxplogb  15681  relogbcxpbap  15682  sgmppw  15709  lgslem1  15722  lgsfvalg  15727  lgsval4  15742  lgsneg  15746  lgsne0  15760  lgsdinn0  15770  lgsquad  15802  funvtxvalg  15880  funiedgvalg  15881  upgrex  15947  uhgr2edg  16050  usgr2v1e2w  16090  iedginwlk  16168  upgrwlkedg  16172  clwwlkccat  16210  clwwlknonex2  16248