Theorem simpr3 1203

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpr3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simpr 485	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜃)
2	1	3ad2antr3 1197	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094

This theorem is referenced by:  simpr13  1266  simpr23  1269  simpr33  1272  simp1r3  1278  simp2r3  1284  simp3r3  1290  3anandis  1479  funopsn  7097  funopsnOLD  7098  fpr2g  7162  isopolem  7296  fr3nr  7722  sexp3  8100  suppfnss  8136  naddass  8629  dif1en  9093  elfir  9325  intrnfi  9326  fisupcl  9380  cnfcomlem  9618  ttrclss  9639  dmttrcl  9640  rnttrcl  9641  ttrclselem2  9645  ackbij1lem15  10153  pwfseqlem4a  10582  pwfseqlem4  10583  eluzuzle  12795  xlesubadd  13213  elioc2  13360  elico2  13361  elicc2  13362  fseq1p1m1  13550  ccatswrd  14629  pfxccat3a  14698  2cshw  14773  tanadd  16132  dvds2ln  16256  prmgaplem5  17024  prmgaplem8  17027  cshwsidrepsw  17062  ressress  17215  f1ovscpbl  17488  mreexexlem4d  17611  mreexexd  17612  2oppccomf  17689  fthmon  17894  fuccocl  17932  fucidcl  17933  invfuc  17942  initoeu2lem1  17979  curf2cl  18195  yonedalem4c  18241  yonedalem3  18244  pospo  18307  latjle12  18414  latjlej1  18417  latnlej2  18423  latlem12  18430  latmlem1  18433  latledi  18441  latjass  18447  latj12  18448  latj32  18449  latj13  18450  latj31  18451  latjrot  18452  latjjdi  18455  latjjdir  18456  latdisdlem  18460  prdssgrpd  18699  prdsmndd  18736  imasmnd2  18740  imasmnd  18741  frmdmnd  18825  grpsubadd  19002  grpaddsubass  19004  grpsubsub4  19007  grppnpcan2  19008  grpnpncan  19009  grpnnncan2  19011  imasgrp2  19029  imasgrp  19030  mulgnndir  19077  mulgnn0dir  19078  mulgnnass  19083  mulgnn0ass  19084  mulgass  19085  pwsmulg  19093  issubg2  19115  qusgrp  19159  kerf1ghm  19220  galcan  19277  gacan  19278  oppgmnd  19327  pmtrprfv  19426  pmtr3ncom  19448  psgnunilem3  19469  frgp0  19733  cmn32  19773  cmn12  19775  abladdsub  19785  ablsubaddsub  19787  ablsubsub23  19797  mulgdi  19799  mulgsubdi  19802  dprdss  20004  dprdf1o  20007  dprdsn  20011  dmdprdsplit  20022  pgpfac1lem5  20054  omndmul2  20106  prdsrngd  20155  imasrng  20156  srgdilem  20171  ringdilem  20228  ringrng  20264  prdsringd  20298  imasring  20308  opprrng  20323  mulgass3  20331  dvrass  20386  dvrdir  20390  subrgunit  20569  issubrg2  20571  isdomn4  20695  abvdiv  20808  lss1  20935  lsssn0  20945  islss3  20956  prdslmodd  20966  islmhm2  21035  lspsolv  21143  lbsextlem4  21161  sralmod  21184  rnglidl1  21232  ipdi  21622  ipsubdir  21624  ipsubdi  21625  ipassr  21628  ipassr2  21629  isphld  21636  ocvlss  21654  sraassab  21850  psrlmod  21941  psrring  21951  psrassa  21954  mpllsslem  21981  mamudm  22385  matring  22433  matassa  22434  ofco2  22441  scmatlss  22515  ma1repveval  22561  mdetunilem1  22602  mdetunilem9  22610  monmatcollpw  22769  iinopn  22892  restopnb  23165  subbascn  23244  hausnei2  23343  nrmsep2  23346  isnrm3  23349  t1sep  23360  regsep2  23366  dnsconst  23368  dfconn2  23409  dislly  23487  tx1stc  23640  qtophmeo  23807  filss  23843  infil  23853  fsubbas  23857  filssufilg  23901  hauspwpwf1  23977  cnextcn  24057  tmdcn2  24079  psmettri  24301  isxmet2d  24317  xmettri  24341  xmetres2  24351  bldisj  24388  blss2ps  24393  blss2  24394  xmstri2  24456  mstri2  24457  xmstri  24458  mstri  24459  xmstri3  24460  mstri3  24461  msrtri  24462  comet  24503  met2ndci  24512  ngprcan  24600  ngplcan  24601  ngpsubcan  24604  nmtri2  24617  nrgdsdi  24655  nrgdsdir  24656  nlmdsdi  24671  nlmdsdir  24672  blcvx  24788  iocopnst  24932  icccvx  24942  pi1grplem  25041  pi1xfrf  25045  pi1cof  25051  clmpm1dir  25095  cmodscmulexp  25114  cvsdiv  25124  cvsdivcl  25125  cphdivcl  25174  cphsubdir  25200  cphsubdi  25201  bcthlem5  25320  rrxcph  25384  volfiniun  25539  volcn  25598  itg1val2  25676  dvconst  25909  dvlip  25985  ftc1a  26029  ulmdvlem3  26392  ang180  26803  cvxcl  26973  scvxcvx  26974  sgmmul  27189  logexprlim  27213  dchrabl  27242  nosupbnd1  27703  noinfbnd1lem5  27716  noinfbnd1  27718  sltssep  27784  addscom  27983  addbday  28035  addsdi  28172  mulsass  28183  motgrp  28636  iscgra1  28903  cgrane2  28906  cgrane4  28908  cgrahl1  28909  cgrahl2  28910  cgracgr  28911  cgratr  28916  cgrabtwn  28919  cgrahl  28920  dfcgra2  28923  sacgr  28924  f1otrge  28965  xmstrkgc  28979  colinearalglem1  29000  colinearalg  29004  axcgrtr  29009  axlowdimlem16  29051  axeuclidlem  29056  axcontlem4  29061  axcontlem7  29064  axcontlem12  29069  eengtrkg  29080  eengtrkge  29081  edglnl  29237  subgruhgredgd  29378  nbfusgrlevtxm2  29472  upgrwlkdvde  29830  crctcshwlkn0lem5  29907  crctcshwlkn0  29914  usgrwwlks2on  30051  umgrwwlks2on  30052  rusgrnumwwlks  30070  clwlkclwwlkfo  30104  3spthd  30271  frgr2wwlkeqm  30426  dlwwlknondlwlknonf1o  30460  numclwwlk5  30483  friendship  30494  grpomuldivass  30637  ablodivdiv4  30650  dipdi  30939  dipsubdi  30945  disjdsct  32802  archiabllem2c  33283  dvrcan5  33324  rloccring  33358  reofld  33433  eqgvscpbl  33440  qusvsval  33442  quslmod  33448  quslmhm  33449  prmidlc  33538  ssdifidl  33547  ssmxidl  33564  ply1degltlss  33686  r1plmhm  33700  drgextlsp  33785  ccfldsrarelvec  33862  constrconj  33936  constrfin  33937  constrelextdg2  33938  pstmfval  34087  qqhval2lem  34172  qqhvq  34178  esumcvg  34277  sigaclcu  34308  measdivcst  34415  measdivcstALTV  34416  carsggect  34509  tgoldbachgtd  34853  bnj970  35136  bnj910  35137  erdszelem9  35434  cvmseu  35511  elmrsubrn  35755  r1peuqusdeg1  35878  cgrid2  36238  btwncomim  36248  btwnswapid  36252  trisegint  36263  cgrxfr  36290  btwnxfr  36291  brofs2  36312  brifs2  36313  endofsegid  36320  btwnconn1lem11  36332  btwnconn2  36337  segcon2  36340  seglemin  36348  segletr  36349  btwnsegle  36352  colinbtwnle  36353  broutsideof2  36357  btwnoutside  36360  broutsideof3  36361  outsideoftr  36364  outsidele  36367  ellines  36387  linethrueu  36391  weiunpo  36700  unbdqndv2  36824  poimirlem28  38022  ftc1anc  38075  sdclem1  38117  sstotbnd2  38148  ismndo1  38247  zerdivemp1x  38321  isdrngo2  38332  iscringd  38372  lsmsat  39507  lfladdcl  39570  lflnegcl  39574  lflvscl  39576  lshpkrlem4  39612  lshpkrlem6  39614  ldualgrplem  39644  lduallmodlem  39651  latmassOLD  39728  latm12  39729  latm32  39730  latmrot  39731  latmmdiN  39733  latmmdir  39734  omlfh1N  39757  omlfh3N  39758  cvrnbtwn2  39774  cvlexchb1  39829  cvlexch3  39831  cvlexch4N  39832  cvlatexchb1  39833  cvlsupr2  39842  hlatjass  39869  hlatj12  39870  hlatj32  39871  cvrat  39921  atcvrj0  39927  cvrat2  39928  atltcvr  39934  atexchltN  39940  cvrat3  39941  cvrat4  39942  atbtwnexOLDN  39946  atbtwnex  39947  3dimlem3  39960  3dimlem3OLDN  39961  3at  39989  2atneat  40014  llncmp  40021  2at0mat0  40024  2atmat0  40025  islpln2a  40047  llncvrlpln  40057  lplncmp  40061  3atnelvolN  40085  4atlem11  40108  lplncvrlvol  40115  lvolcmp  40116  2atm2atN  40284  elpaddatriN  40302  elpadd2at2  40306  paddasslem8  40326  paddasslem17  40335  paddass  40337  padd12N  40338  paddssw1  40342  pmodlem2  40346  pmodN  40349  pmapjlln1  40354  atmod1i2  40358  pexmidlem2N  40470  pexmidlem7N  40475  pl42lem2N  40479  pl42lem3N  40480  pl42lem4N  40481  pl42N  40482  lhp2lt  40500  lhpm0atN  40528  lautlt  40590  lautcvr  40591  lautj  40592  lautm  40593  ltrneq2  40647  cdleme1b  40725  cdleme3b  40728  cdleme3c  40729  cdleme9b  40751  cdlemefs27cl  40912  cdleme42mN  40986  cdlemg4c  41111  trljco  41239  tgrpgrplem  41248  tendoplass  41282  tendodi1  41283  tendodi2  41284  erngplus2  41303  erngplus2-rN  41311  cdlemk36  41412  erngdvlem3  41489  erngdvlem3-rN  41497  dvaplusgv  41509  tendospass  41518  tendospdi1  41519  dvalveclem  41524  dialss  41545  dvhvaddass  41596  dvhopvsca  41601  dvhlveclem  41607  diblss  41669  diclss  41692  diclspsn  41693  cdlemn11pre  41709  dihmeetlem12N  41817  dihmeetlem16N  41821  dihmeetlem17N  41822  dvh4dimN  41946  lpolsatN  41987  lpolpolsatN  41988  dochpolN  41989  lclkr  42032  lclkrs  42038  lcfr  42084  lcmineqlem13  42533  aks6d1c1  42608  irrapxlem6  43279  jm2.26lem3  43453  mpaamn  43608  mendring  43640  mendlmod  43641  mendassa  43642  nnoeomeqom  43764  omabs2  43784  neicvgel1  44570  rfcnpre4  45489  fmuldfeq  46035  stoweidlem43  46493  stoweidlem52  46502  stoweidlem53  46503  stoweidlem56  46506  issmfgt  47206  issmfge  47220  iccelpart  47915  prproropf1olem1  47985  fmtnoprmfac1  48050  fmtnoprmfac2  48052  isubgr3stgrlem2  48465  isubgr3stgrlem4  48467  grlimgrtrilem1  48499  copissgrp  48666  cznrng  48759  funcringcsetcALTV2lem9  48796  funcringcsetclem9ALTV  48819  linccl  48912  lincsumscmcl  48931  ldepsprlem  48970  lincresunit3lem1  48977  itsclc0yqe  49259  resipos  49472  topdlat  49501  catprs  49508  endmndlem  49512  idmon  49517  idepi  49518  thincmon  49930  thincepi  49931  functhinclem1  49941  grptcmon  50090  grptcepi  50091