Theorem simpr3 1215

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr13  1278  simpr23  1281  simpr33  1284  simp1r3  1290  simp2r3  1296  simp3r3  1302  3anandis  1500  funopsn  7148  funopsnOLD  7149  fpr2g  7214  isopolem  7350  fr3nr  7775  sexp3  8155  suppfnss  8191  naddass  8689  dif1en  9160  elfir  9389  intrnfi  9390  fisupcl  9444  cnfcomlem  9682  ttrclss  9703  dmttrcl  9704  rnttrcl  9705  ttrclselem2  9709  ackbij1lem15  10239  pwfseqlem4a  10674  pwfseqlem4  10675  eluzuzle  12900  xlesubadd  13319  elioc2  13466  elico2  13467  elicc2  13468  fseq1p1m1  13657  ccatswrd  14742  pfxccat3a  14811  2cshw  14888  tanadd  16261  dvds2ln  16385  prmgaplem5  17153  prmgaplem8  17156  cshwsidrepsw  17191  ressress  17345  f1ovscpbl  17618  mreexexlem4d  17741  mreexexd  17742  2oppccomf  17819  fthmon  18024  fuccocl  18062  fucidcl  18063  invfuc  18072  initoeu2lem1  18109  curf2cl  18325  yonedalem4c  18371  yonedalem3  18374  pospo  18437  latjle12  18544  latjlej1  18547  latnlej2  18553  latlem12  18560  latmlem1  18563  latledi  18571  latjass  18577  latj12  18578  latj32  18579  latj13  18580  latj31  18581  latjrot  18582  latjjdi  18585  latjjdir  18586  latdisdlem  18590  prdssgrpd  18841  prdsmndd  18883  imasmnd2  18887  imasmnd  18888  frmdmnd  18974  grpsubadd  19157  grpaddsubass  19159  grpsubsub4  19162  grppnpcan2  19163  grpnpncan  19164  grpnnncan2  19166  imasgrp2  19184  imasgrp  19185  mulgnndir  19232  mulgnn0dir  19233  mulgnnass  19238  mulgnn0ass  19239  mulgass  19240  pwsmulg  19248  issubg2  19271  qusgrp  19320  kerf1ghm  19380  galcan  19437  gacan  19438  oppgmnd  19487  pmtrprfv  19586  pmtr3ncom  19608  psgnunilem3  19629  frgp0  19893  cmn32  19933  cmn12  19935  abladdsub  19945  ablsubaddsub  19947  ablsubsub23  19957  mulgdi  19959  mulgsubdi  19962  dprdss  20164  dprdf1o  20167  dprdsn  20171  dmdprdsplit  20182  pgpfac1lem5  20214  omndmul2  20266  prdsrngd  20317  imasrng  20318  srgdilem  20337  ringdilem  20394  ringrng  20432  prdsringd  20467  imasring  20477  opprrng  20492  mulgass3  20500  dvrass  20555  dvrdir  20559  subrgunit  20758  issubrg2  20760  isdomn4  20883  abvdiv  21001  lss1  21128  lsssn0  21138  islss3  21149  prdslmodd  21159  islmhm2  21228  lspsolv  21336  lbsextlem4  21354  sralmod  21377  rnglidl1  21427  prmidlc  21542  ssdifidl  21554  ipdi  21859  ipsubdir  21861  ipsubdi  21862  ipassr  21865  ipassr2  21866  isphld  21873  ocvlss  21891  sraassab  22089  psrlmod  22180  psrring  22190  psrassa  22193  mpllsslem  22220  mamudm  22623  matring  22671  matassa  22672  ofco2  22679  scmatlss  22753  ma1repveval  22799  mdetunilem1  22840  mdetunilem9  22848  monmatcollpw  23010  iinopn  23133  restopnb  23406  subbascn  23485  hausnei2  23584  nrmsep2  23587  isnrm3  23590  t1sep  23601  regsep2  23607  dnsconst  23609  dfconn2  23650  dislly  23729  tx1stc  23882  qtophmeo  24049  filss  24085  infil  24095  fsubbas  24099  filssufilg  24143  hauspwpwf1  24219  cnextcn  24299  tmdcn2  24321  psmettri  24543  isxmet2d  24559  xmettri  24583  xmetres2  24593  bldisj  24630  blss2ps  24635  blss2  24636  xmstri2  24698  mstri2  24699  xmstri  24700  mstri  24701  xmstri3  24702  mstri3  24703  msrtri  24704  comet  24745  met2ndci  24754  ngprcan  24842  ngplcan  24843  ngpsubcan  24846  nmtri2  24859  nrgdsdi  24897  nrgdsdir  24898  nlmdsdi  24913  nlmdsdir  24914  blcvx  25030  iocopnst  25174  icccvx  25184  pi1grplem  25283  pi1xfrf  25287  pi1cof  25293  clmpm1dir  25337  cmodscmulexp  25356  cvsdiv  25366  cvsdivcl  25367  cphdivcl  25416  cphsubdir  25442  cphsubdi  25443  bcthlem5  25562  rrxcph  25626  volfiniun  25781  volcn  25840  itg1val2  25918  dvconst  26151  dvlip  26227  ftc1a  26271  ulmdvlem3  26645  ang180  27059  cvxcl  27229  scvxcvx  27230  sgmmul  27445  logexprlim  27469  dchrabl  27498  nosupbnd1  27958  noinfbnd1lem5  27971  noinfbnd1  27973  sltssep  28040  addscom  28239  addbday  28291  addsdi  28428  mulsass  28439  motgrp  28893  iscgra1  29204  cgrane2  29207  cgrane4  29209  cgrahl1  29210  cgrahl2  29211  cgracgr  29212  cgratr  29217  cgrabtwn  29221  cgrahl  29222  dfcgra2  29225  sacgr  29226  angmgmaddcl  29278  f1otrge  29336  xmstrkgc  29350  colinearalglem1  29371  colinearalg  29375  axcgrtr  29380  axlowdimlem16  29422  axeuclidlem  29427  axcontlem4  29432  axcontlem7  29435  axcontlem12  29440  eengtrkg  29451  eengtrkge  29452  edglnl  29608  subgruhgredgd  29752  nbfusgrlevtxm2  29846  upgrwlkdvde  30210  crctcshwlkn0lem5  30290  crctcshwlkn0  30297  usgrwwlks2on  30434  umgrwwlks2on  30435  rusgrnumwwlks  30453  clwlkclwwlkfo  30487  3spthd  30664  frgr2wwlkeqm  30819  dlwwlknondlwlknonf1o  30853  numclwwlk5  30876  friendship  30887  grpomuldivass  31030  ablodivdiv4  31043  dipdi  31332  dipsubdi  31338  disjdsct  33183  archiabllem2c  33643  dvrcan5  33683  rloccring  33719  reofld  33791  eqgvscpbl  33798  qusvsval  33800  quslmod  33806  quslmhm  33807  ssmxidl  33885  ply1degltlss  34014  r1plmhm  34027  drgextlsp  34112  ccfldsrarelvec  34189  constrconj  34263  constrfin  34264  constrelextdg2  34265  pstmfval  34414  qqhval2lem  34499  qqhvq  34505  esumcvg  34604  sigaclcu  34635  measdivcst  34743  measdivcstALTV  34744  carsggect  34837  tgoldbachgtd  35178  bnj970  35464  bnj910  35465  erdszelem9  35786  cvmseu  35863  elmrsubrn  36107  r1peuqusdeg1  36230  cgrid2  36591  btwncomim  36601  btwnswapid  36605  trisegint  36616  cgrxfr  36643  btwnxfr  36644  brofs2  36665  brifs2  36666  endofsegid  36673  btwnconn1lem11  36685  btwnconn2  36690  segcon2  36693  seglemin  36701  segletr  36702  btwnsegle  36705  colinbtwnle  36706  broutsideof2  36710  btwnoutside  36713  broutsideof3  36714  outsideoftr  36717  outsidele  36720  ellines  36740  linethrueu  36744  nmulprop  36778  nadddi  36812  weiunpo  37092  unbdqndv2  37216  poimirlem28  38405  ftc1anc  38458  sdclem1  38501  sstotbnd2  38532  ismndo1  38631  zerdivemp1x  38705  isdrngo2  38716  iscringd  38756  lsmsat  39889  lfladdcl  39952  lflnegcl  39956  lflvscl  39958  lshpkrlem4  39994  lshpkrlem6  39996  ldualgrplem  40026  lduallmodlem  40033  latmassOLD  40110  latm12  40111  latm32  40112  latmrot  40113  latmmdiN  40115  latmmdir  40116  omlfh1N  40139  omlfh3N  40140  cvrnbtwn2  40156  cvlexchb1  40211  cvlexch3  40213  cvlexch4N  40214  cvlatexchb1  40215  cvlsupr2  40224  hlatjass  40251  hlatj12  40252  hlatj32  40253  cvrat  40303  atcvrj0  40309  cvrat2  40310  atltcvr  40316  atexchltN  40322  cvrat3  40323  cvrat4  40324  atbtwnexOLDN  40328  atbtwnex  40329  3dimlem3  40342  3dimlem3OLDN  40343  3at  40371  2atneat  40396  llncmp  40403  2at0mat0  40406  2atmat0  40407  islpln2a  40429  llncvrlpln  40439  lplncmp  40443  3atnelvolN  40467  4atlem11  40490  lplncvrlvol  40497  lvolcmp  40498  2atm2atN  40666  elpaddatriN  40684  elpadd2at2  40688  paddasslem8  40708  paddasslem17  40717  paddass  40719  padd12N  40720  paddssw1  40724  pmodlem2  40728  pmodN  40731  pmapjlln1  40736  atmod1i2  40740  pexmidlem2N  40852  pexmidlem7N  40857  pl42lem2N  40861  pl42lem3N  40862  pl42lem4N  40863  pl42N  40864  lhp2lt  40882  lhpm0atN  40910  lautlt  40972  lautcvr  40973  lautj  40974  lautm  40975  ltrneq2  41029  cdleme1b  41107  cdleme3b  41110  cdleme3c  41111  cdleme9b  41133  cdlemefs27cl  41294  cdleme42mN  41368  cdlemg4c  41493  trljco  41621  tgrpgrplem  41630  tendoplass  41664  tendodi1  41665  tendodi2  41666  erngplus2  41685  erngplus2-rN  41693  cdlemk36  41794  erngdvlem3  41871  erngdvlem3-rN  41879  dvaplusgv  41891  tendospass  41900  tendospdi1  41901  dvalveclem  41906  dialss  41927  dvhvaddass  41978  dvhopvsca  41983  dvhlveclem  41989  diblss  42051  diclss  42074  diclspsn  42075  cdlemn11pre  42091  dihmeetlem12N  42199  dihmeetlem16N  42203  dihmeetlem17N  42204  dvh4dimN  42328  lpolsatN  42369  lpolpolsatN  42370  dochpolN  42371  lclkr  42414  lclkrs  42420  lcfr  42466  lcmineqlem13  42915  aks6d1c1  42990  irrapxlem6  43676  jm2.26lem3  43850  mpaamn  44005  mendring  44037  mendlmod  44038  mendassa  44039  nnoeomeqom  44161  omabs2  44181  neicvgel1  44967  rfcnpre4  45876  fmuldfeq  46421  stoweidlem43  46879  stoweidlem52  46888  stoweidlem53  46889  stoweidlem56  46892  issmfgt  47592  issmfge  47606  tmachlem-franscan  47785  iccelpart  48341  prproropf1olem1  48411  fmtnoprmfac1  48476  fmtnoprmfac2  48478  isubgr3stgrlem2  48891  isubgr3stgrlem4  48893  grlimgrtrilem1  48925  copissgrp  49091  cznrng  49184  funcringcsetcALTV2lem9  49221  funcringcsetclem9ALTV  49244  idomcanl  49270  linccl  49352  lincsumscmcl  49371  ldepsprlem  49410  lincresunit3lem1  49417  itsclc0yqe  49699  resipos  49909  topdlat  49938  catprs  49945  endmndlem  49949  idmon  49954  idepi  49955  thincmon  50367  thincepi  50368  functhinclem1  50378  grptcmon  50527  grptcepi  50528  nellindf  50811