Theorem simpr3 1176

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  simpr13  1239  simpr23  1242  simpr33  1245  simp1r3  1251  simp2r3  1257  simp3r3  1263  3anandis  1450  funopsn  6727  fpr2g  6794  isopolem  6915  fr3nr  7304  suppfnss  7651  elfir  8666  intrnfi  8667  fisupcl  8720  cnfcomlem  8948  ackbij1lem15  9446  pwfseqlem4a  9873  pwfseqlem4  9874  eluzuzle  12060  xlesubadd  12465  elioc2  12608  elico2  12609  elicc2  12610  fseq1p1m1  12790  ccatswrd  13839  pfxccat3a  13932  tanadd  15370  dvds2ln  15492  prmgaplem5  16237  prmgaplem8  16240  cshwsidrepsw  16273  ressress  16408  f1ovscpbl  16645  mreexexlem4d  16766  mreexexd  16767  2oppccomf  16843  fthmon  17045  fuccocl  17082  fucidcl  17083  invfuc  17092  initoeu2lem1  17122  curf2cl  17329  yonedalem4c  17375  yonedalem3  17378  pospo  17431  latjle12  17520  latjlej1  17523  latnlej2  17529  latlem12  17536  latmlem1  17539  latledi  17547  latjass  17553  latj12  17554  latj32  17555  latj13  17556  latj31  17557  latjrot  17558  latjjdi  17561  latjjdir  17562  latdisdlem  17647  prdsmndd  17781  imasmnd2  17785  imasmnd  17786  frmdmnd  17855  grpsubadd  17964  grpaddsubass  17966  grpsubsub4  17969  grppnpcan2  17970  grpnpncan  17971  grpnnncan2  17973  imasgrp2  17991  imasgrp  17992  mulgnndir  18030  mulgnn0dir  18031  mulgnnass  18036  mulgnn0ass  18037  mulgass  18038  pwsmulg  18046  issubg2  18068  qusgrp  18108  galcan  18195  gacan  18196  oppgmnd  18243  symggrp  18279  pmtrprfv  18332  pmtr3ncom  18354  psgnunilem3  18376  frgp0  18636  cmn32  18674  cmn12  18676  abladdsub  18683  ablsubsub23  18693  mulgdi  18695  mulgsubdi  18698  dprdss  18891  dprdf1o  18894  dprdsn  18898  dmdprdsplit  18909  pgpfac1lem5  18941  srgi  18974  ringi  19023  prdsringd  19075  imasring  19082  opprring  19094  mulgass3  19100  dvrass  19153  kerf1ghm  19210  kerf1hrmOLD  19211  subrgunit  19266  issubrg2  19268  abvdiv  19320  lss1  19422  lsssn0  19431  islss3  19443  prdslmodd  19453  islmhm2  19522  lspsolv  19627  lbsextlem4  19645  sralmod  19671  issubassa  19808  sraassa  19809  psrbaglesupp  19852  psrbagcon  19855  psrgrp  19882  psrlmod  19885  psrring  19895  psrassa  19898  mpllsslem  19919  ipdi  20476  ipsubdir  20478  ipsubdi  20479  ipassr  20482  ipassr2  20483  isphld  20490  ocvlss  20508  mamudm  20691  matring  20746  matassa  20747  ofco2  20754  scmatlss  20828  ma1repveval  20874  mdetunilem1  20915  mdetunilem9  20923  monmatcollpw  21081  iinopn  21204  restopnb  21477  subbascn  21556  hausnei2  21655  nrmsep2  21658  isnrm3  21661  t1sep  21672  regsep2  21678  dnsconst  21680  dfconn2  21721  dislly  21799  tx1stc  21952  qtophmeo  22119  filss  22155  infil  22165  fsubbas  22169  filssufilg  22213  hauspwpwf1  22289  cnextcn  22369  tmdcn2  22391  psmettri  22614  isxmet2d  22630  xmettri  22654  xmetres2  22664  bldisj  22701  blss2ps  22706  blss2  22707  xmstri2  22769  mstri2  22770  xmstri  22771  mstri  22772  xmstri3  22773  mstri3  22774  msrtri  22775  comet  22816  met2ndci  22825  ngprcan  22912  ngplcan  22913  ngpsubcan  22916  nmtri2  22929  nrgdsdi  22967  nrgdsdir  22968  nlmdsdi  22983  nlmdsdir  22984  blcvx  23099  iocopnst  23237  icccvx  23247  pi1grplem  23346  pi1xfrf  23350  pi1cof  23356  clmpm1dir  23400  cmodscmulexp  23419  cvsdiv  23429  cvsdivcl  23430  cphdivcl  23479  cphsubdir  23505  cphsubdi  23506  bcthlem5  23624  rrxcph  23688  volfiniun  23841  volcn  23900  itg1val2  23978  dvconst  24207  dvlip  24283  ftc1a  24327  ulmdvlem3  24683  ang180  25083  cvxcl  25254  scvxcvx  25255  sgmmul  25469  logexprlim  25493  dchrabl  25522  motgrp  26021  iscgra1  26288  cgrane2  26291  cgrane4  26293  cgrahl1  26294  cgrahl2  26295  cgracgr  26296  cgratr  26301  cgrabtwn  26304  cgrahl  26305  dfcgra2  26308  sacgr  26309  sacgrOLD  26310  f1otrge  26351  xmstrkgc  26365  colinearalglem1  26385  colinearalg  26389  axcgrtr  26394  axlowdimlem16  26436  axeuclidlem  26441  axcontlem4  26446  axcontlem7  26449  axcontlem12  26454  eengtrkg  26465  eengtrkge  26466  edglnl  26621  subgruhgredgd  26759  nbfusgrlevtxm2  26853  upgrwlkdvde  27216  crctcshwlkn0lem5  27290  crctcshwlkn0  27297  umgrwwlks2on  27453  rusgrnumwwlks  27470  rusgrnumwwlksOLD  27471  clwlkclwwlkfoOLD  27509  clwlkclwwlkfo  27513  3spthd  27695  frgr2wwlkeqm  27855  dlwwlknondlwlknonf1o  27906  dlwwlknondlwlknonf1oOLD  27907  numclwwlk5  27935  friendship  27946  grpomuldivass  28085  ablodivdiv4  28098  dipdi  28387  dipsubdi  28393  disjdsct  30179  omndmul2  30409  archiabllem2c  30446  dvrdir  30496  dvrcan5  30499  reofld  30548  eqgvscpbl  30554  qusscaval  30556  quslmod  30558  quslmhm  30559  drgextlsp  30581  ccfldsrarelvec  30641  pstmfval  30737  qqhval2lem  30823  qqhvq  30829  esumcvg  30946  sigaclcu  30978  measdivcstOLD  31085  measdivcst  31086  carsggect  31178  tgoldbachgtd  31542  bnj970  31827  bnj910  31828  erdszelem9  31991  cvmseu  32068  elmrsubrn  32227  noprefixmo  32663  nosupbnd1  32675  ssltsep  32720  cgrid2  32925  btwncomim  32935  btwnswapid  32939  trisegint  32950  cgrxfr  32977  btwnxfr  32978  brofs2  32999  brifs2  33000  endofsegid  33007  btwnconn1lem11  33019  btwnconn2  33024  segcon2  33027  seglemin  33035  segletr  33036  btwnsegle  33039  colinbtwnle  33040  broutsideof2  33044  btwnoutside  33047  broutsideof3  33048  outsideoftr  33051  outsidele  33054  ellines  33074  linethrueu  33078  unbdqndv2  33310  poimirlem28  34309  ftc1anc  34364  sdclem1  34408  sstotbnd2  34442  ismndo1  34541  zerdivemp1x  34615  isdrngo2  34626  iscringd  34666  lsmsat  35537  lfladdcl  35600  lflnegcl  35604  lflvscl  35606  lshpkrlem4  35642  lshpkrlem6  35644  ldualgrplem  35674  lduallmodlem  35681  latmassOLD  35758  latm12  35759  latm32  35760  latmrot  35761  latmmdiN  35763  latmmdir  35764  omlfh1N  35787  omlfh3N  35788  cvrnbtwn2  35804  cvlexchb1  35859  cvlexch3  35861  cvlexch4N  35862  cvlatexchb1  35863  cvlsupr2  35872  hlatjass  35899  hlatj12  35900  hlatj32  35901  cvrat  35951  atcvrj0  35957  cvrat2  35958  atltcvr  35964  atexchltN  35970  cvrat3  35971  cvrat4  35972  atbtwnexOLDN  35976  atbtwnex  35977  3dimlem3  35990  3dimlem3OLDN  35991  3at  36019  2atneat  36044  llncmp  36051  2at0mat0  36054  2atmat0  36055  islpln2a  36077  llncvrlpln  36087  lplncmp  36091  3atnelvolN  36115  4atlem11  36138  lplncvrlvol  36145  lvolcmp  36146  2atm2atN  36314  elpaddatriN  36332  elpadd2at2  36336  paddasslem8  36356  paddasslem17  36365  paddass  36367  padd12N  36368  paddssw1  36372  pmodlem2  36376  pmodN  36379  pmapjlln1  36384  atmod1i2  36388  pexmidlem2N  36500  pexmidlem7N  36505  pl42lem2N  36509  pl42lem3N  36510  pl42lem4N  36511  pl42N  36512  lhp2lt  36530  lhpm0atN  36558  lautlt  36620  lautcvr  36621  lautj  36622  lautm  36623  ltrneq2  36677  cdleme1b  36755  cdleme3b  36758  cdleme3c  36759  cdleme9b  36781  cdlemefs27cl  36942  cdleme42mN  37016  cdlemg4c  37141  trljco  37269  tgrpgrplem  37278  tendoplass  37312  tendodi1  37313  tendodi2  37314  erngplus2  37333  erngplus2-rN  37341  cdlemk36  37442  erngdvlem3  37519  erngdvlem3-rN  37527  dvaplusgv  37539  tendospass  37548  tendospdi1  37549  dvalveclem  37554  dialss  37575  dvhvaddass  37626  dvhopvsca  37631  dvhlveclem  37637  diblss  37699  diclss  37722  diclspsn  37723  cdlemn11pre  37739  dihmeetlem12N  37847  dihmeetlem16N  37851  dihmeetlem17N  37852  dvh4dimN  37976  lpolsatN  38017  lpolpolsatN  38018  dochpolN  38019  lclkr  38062  lclkrs  38068  lcfr  38114  irrapxlem6  38765  jm2.26lem3  38939  mpaamn  39097  mendring  39133  mendlmod  39134  mendassa  39135  neicvgel1  39777  rfcnpre4  40654  fmuldfeq  41241  stoweidlem43  41705  stoweidlem52  41714  stoweidlem53  41715  stoweidlem56  41718  issmfgt  42410  issmfge  42423  iccelpart  42911  prproropf1olem1  42973  fmtnoprmfac1  43035  fmtnoprmfac2  43037  copissgrp  43383  ringrng  43454  cznrng  43530  funcringcsetcALTV2lem9  43619  funcringcsetclem9ALTV  43642  linccl  43776  lincsumscmcl  43795  ldepsprlem  43834  lincresunit3lem1  43841  itsclc0yqe  44056