Theorem simpr3 1194

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 484	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜃)
2	1	3ad2antr3 1188	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simpr13  1257  simpr23  1260  simpr33  1263  simp1r3  1269  simp2r3  1275  simp3r3  1281  3anandis  1468  funopsn  7157  fpr2g  7223  isopolem  7353  fr3nr  7774  sexp3  8158  suppfnss  8194  naddass  8717  dif1en  9185  elfir  9439  intrnfi  9440  fisupcl  9493  cnfcomlem  9723  ttrclss  9744  dmttrcl  9745  rnttrcl  9746  ttrclselem2  9750  ackbij1lem15  10258  pwfseqlem4a  10685  pwfseqlem4  10686  eluzuzle  12862  xlesubadd  13275  elioc2  13420  elico2  13421  elicc2  13422  fseq1p1m1  13608  ccatswrd  14651  pfxccat3a  14721  2cshw  14796  tanadd  16144  dvds2ln  16266  prmgaplem5  17024  prmgaplem8  17027  cshwsidrepsw  17063  ressress  17229  f1ovscpbl  17508  mreexexlem4d  17627  mreexexd  17628  2oppccomf  17707  fthmon  17916  fuccocl  17956  fucidcl  17957  invfuc  17966  initoeu2lem1  18003  curf2cl  18223  yonedalem4c  18269  yonedalem3  18272  pospo  18337  latjle12  18442  latjlej1  18445  latnlej2  18451  latlem12  18458  latmlem1  18461  latledi  18469  latjass  18475  latj12  18476  latj32  18477  latj13  18478  latj31  18479  latjrot  18480  latjjdi  18483  latjjdir  18484  latdisdlem  18488  prdssgrpd  18693  prdsmndd  18727  imasmnd2  18731  imasmnd  18732  frmdmnd  18811  grpsubadd  18984  grpaddsubass  18986  grpsubsub4  18989  grppnpcan2  18990  grpnpncan  18991  grpnnncan2  18993  imasgrp2  19011  imasgrp  19012  mulgnndir  19058  mulgnn0dir  19059  mulgnnass  19064  mulgnn0ass  19065  mulgass  19066  pwsmulg  19074  issubg2  19096  qusgrp  19141  kerf1ghm  19201  galcan  19255  gacan  19256  oppgmnd  19308  pmtrprfv  19408  pmtr3ncom  19430  psgnunilem3  19451  frgp0  19715  cmn32  19755  cmn12  19757  abladdsub  19767  ablsubaddsub  19769  ablsubsub23  19779  mulgdi  19781  mulgsubdi  19784  dprdss  19986  dprdf1o  19989  dprdsn  19993  dmdprdsplit  20004  pgpfac1lem5  20036  prdsrngd  20116  imasrng  20117  srgdilem  20132  ringdilem  20189  ringrng  20221  prdsringd  20257  imasring  20266  opprrng  20284  mulgass3  20292  dvrass  20347  dvrdir  20351  subrgunit  20529  issubrg2  20531  abvdiv  20717  lss1  20822  lsssn0  20832  islss3  20843  prdslmodd  20853  islmhm2  20923  lspsolv  21031  lbsextlem4  21049  sralmod  21080  rnglidl1  21128  isdomn4  21250  ipdi  21572  ipsubdir  21574  ipsubdi  21575  ipassr  21578  ipassr2  21579  isphld  21586  ocvlss  21604  sraassab  21801  sraassaOLD  21803  psrbaglesuppOLD  21858  psrbagconOLD  21864  psrgrpOLD  21900  psrlmod  21903  psrring  21913  psrassa  21916  mpllsslem  21942  mamudm  22303  matring  22358  matassa  22359  ofco2  22366  scmatlss  22440  ma1repveval  22486  mdetunilem1  22527  mdetunilem9  22535  monmatcollpw  22694  iinopn  22817  restopnb  23092  subbascn  23171  hausnei2  23270  nrmsep2  23273  isnrm3  23276  t1sep  23287  regsep2  23293  dnsconst  23295  dfconn2  23336  dislly  23414  tx1stc  23567  qtophmeo  23734  filss  23770  infil  23780  fsubbas  23784  filssufilg  23828  hauspwpwf1  23904  cnextcn  23984  tmdcn2  24006  psmettri  24230  isxmet2d  24246  xmettri  24270  xmetres2  24280  bldisj  24317  blss2ps  24322  blss2  24323  xmstri2  24385  mstri2  24386  xmstri  24387  mstri  24388  xmstri3  24389  mstri3  24390  msrtri  24391  comet  24435  met2ndci  24444  ngprcan  24532  ngplcan  24533  ngpsubcan  24536  nmtri2  24549  nrgdsdi  24595  nrgdsdir  24596  nlmdsdi  24611  nlmdsdir  24612  blcvx  24727  iocopnst  24877  icccvx  24888  pi1grplem  24989  pi1xfrf  24993  pi1cof  24999  clmpm1dir  25043  cmodscmulexp  25062  cvsdiv  25072  cvsdivcl  25073  cphdivcl  25123  cphsubdir  25149  cphsubdi  25150  bcthlem5  25269  rrxcph  25333  volfiniun  25489  volcn  25548  itg1val2  25626  dvconst  25859  dvlip  25939  ftc1a  25985  ulmdvlem3  26351  ang180  26759  cvxcl  26930  scvxcvx  26931  sgmmul  27147  logexprlim  27171  dchrabl  27200  nosupbnd1  27660  noinfbnd1lem5  27673  noinfbnd1  27675  ssltsep  27736  addscom  27896  addsdi  28068  mulsass  28079  motgrp  28360  iscgra1  28627  cgrane2  28630  cgrane4  28632  cgrahl1  28633  cgrahl2  28634  cgracgr  28635  cgratr  28640  cgrabtwn  28643  cgrahl  28644  dfcgra2  28647  sacgr  28648  f1otrge  28689  xmstrkgc  28709  colinearalglem1  28730  colinearalg  28734  axcgrtr  28739  axlowdimlem16  28781  axeuclidlem  28786  axcontlem4  28791  axcontlem7  28794  axcontlem12  28799  eengtrkg  28810  eengtrkge  28811  edglnl  28969  subgruhgredgd  29110  nbfusgrlevtxm2  29204  upgrwlkdvde  29564  crctcshwlkn0lem5  29638  crctcshwlkn0  29645  umgrwwlks2on  29781  rusgrnumwwlks  29798  clwlkclwwlkfo  29832  3spthd  29999  frgr2wwlkeqm  30154  dlwwlknondlwlknonf1o  30188  numclwwlk5  30211  friendship  30222  grpomuldivass  30364  ablodivdiv4  30377  dipdi  30666  dipsubdi  30672  disjdsct  32495  omndmul2  32805  archiabllem2c  32916  dvrcan5  32957  rloccring  32997  reofld  33069  eqgvscpbl  33075  qusvsval  33077  quslmod  33083  quslmhm  33084  prmidlc  33177  ssmxidl  33200  ply1degltlss  33267  r1plmhm  33280  drgextlsp  33293  ccfldsrarelvec  33359  pstmfval  33497  qqhval2lem  33582  qqhvq  33588  esumcvg  33705  sigaclcu  33736  measdivcst  33843  measdivcstALTV  33844  carsggect  33938  tgoldbachgtd  34294  bnj970  34578  bnj910  34579  erdszelem9  34809  cvmseu  34886  elmrsubrn  35130  cgrid2  35599  btwncomim  35609  btwnswapid  35613  trisegint  35624  cgrxfr  35651  btwnxfr  35652  brofs2  35673  brifs2  35674  endofsegid  35681  btwnconn1lem11  35693  btwnconn2  35698  segcon2  35701  seglemin  35709  segletr  35710  btwnsegle  35713  colinbtwnle  35714  broutsideof2  35718  btwnoutside  35721  broutsideof3  35722  outsideoftr  35725  outsidele  35728  ellines  35748  linethrueu  35752  unbdqndv2  35986  poimirlem28  37121  ftc1anc  37174  sdclem1  37216  sstotbnd2  37247  ismndo1  37346  zerdivemp1x  37420  isdrngo2  37431  iscringd  37471  lsmsat  38480  lfladdcl  38543  lflnegcl  38547  lflvscl  38549  lshpkrlem4  38585  lshpkrlem6  38587  ldualgrplem  38617  lduallmodlem  38624  latmassOLD  38701  latm12  38702  latm32  38703  latmrot  38704  latmmdiN  38706  latmmdir  38707  omlfh1N  38730  omlfh3N  38731  cvrnbtwn2  38747  cvlexchb1  38802  cvlexch3  38804  cvlexch4N  38805  cvlatexchb1  38806  cvlsupr2  38815  hlatjass  38842  hlatj12  38843  hlatj32  38844  cvrat  38895  atcvrj0  38901  cvrat2  38902  atltcvr  38908  atexchltN  38914  cvrat3  38915  cvrat4  38916  atbtwnexOLDN  38920  atbtwnex  38921  3dimlem3  38934  3dimlem3OLDN  38935  3at  38963  2atneat  38988  llncmp  38995  2at0mat0  38998  2atmat0  38999  islpln2a  39021  llncvrlpln  39031  lplncmp  39035  3atnelvolN  39059  4atlem11  39082  lplncvrlvol  39089  lvolcmp  39090  2atm2atN  39258  elpaddatriN  39276  elpadd2at2  39280  paddasslem8  39300  paddasslem17  39309  paddass  39311  padd12N  39312  paddssw1  39316  pmodlem2  39320  pmodN  39323  pmapjlln1  39328  atmod1i2  39332  pexmidlem2N  39444  pexmidlem7N  39449  pl42lem2N  39453  pl42lem3N  39454  pl42lem4N  39455  pl42N  39456  lhp2lt  39474  lhpm0atN  39502  lautlt  39564  lautcvr  39565  lautj  39566  lautm  39567  ltrneq2  39621  cdleme1b  39699  cdleme3b  39702  cdleme3c  39703  cdleme9b  39725  cdlemefs27cl  39886  cdleme42mN  39960  cdlemg4c  40085  trljco  40213  tgrpgrplem  40222  tendoplass  40256  tendodi1  40257  tendodi2  40258  erngplus2  40277  erngplus2-rN  40285  cdlemk36  40386  erngdvlem3  40463  erngdvlem3-rN  40471  dvaplusgv  40483  tendospass  40492  tendospdi1  40493  dvalveclem  40498  dialss  40519  dvhvaddass  40570  dvhopvsca  40575  dvhlveclem  40581  diblss  40643  diclss  40666  diclspsn  40667  cdlemn11pre  40683  dihmeetlem12N  40791  dihmeetlem16N  40795  dihmeetlem17N  40796  dvh4dimN  40920  lpolsatN  40961  lpolpolsatN  40962  dochpolN  40963  lclkr  41006  lclkrs  41012  lcfr  41058  lcmineqlem13  41512  aks6d1c1  41587  irrapxlem6  42247  jm2.26lem3  42422  mpaamn  42580  mendring  42616  mendlmod  42617  mendassa  42618  nnoeomeqom  42741  omabs2  42761  neicvgel1  43549  rfcnpre4  44396  fmuldfeq  44971  stoweidlem43  45431  stoweidlem52  45440  stoweidlem53  45441  stoweidlem56  45444  issmfgt  46144  issmfge  46158  iccelpart  46773  prproropf1olem1  46843  fmtnoprmfac1  46905  fmtnoprmfac2  46907  copissgrp  47230  cznrng  47323  funcringcsetcALTV2lem9  47360  funcringcsetclem9ALTV  47383  linccl  47482  lincsumscmcl  47501  ldepsprlem  47540  lincresunit3lem1  47547  itsclc0yqe  47834  topdlat  48015  catprs  48017  endmndlem  48021  idmon  48022  idepi  48023  thincmon  48040  thincepi  48041  functhinclem1  48047  grptcmon  48102  grptcepi  48103