Theorem simpr3 1192

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpr13  1255  simpr23  1258  simpr33  1261  simp1r3  1267  simp2r3  1273  simp3r3  1279  3anandis  1467  funopsn  6910  fpr2g  6974  isopolem  7098  fr3nr  7494  suppfnss  7855  elfir  8879  intrnfi  8880  fisupcl  8933  cnfcomlem  9162  ackbij1lem15  9656  pwfseqlem4a  10083  pwfseqlem4  10084  eluzuzle  12253  xlesubadd  12657  elioc2  12800  elico2  12801  elicc2  12802  fseq1p1m1  12982  ccatswrd  14030  pfxccat3a  14100  2cshw  14175  tanadd  15520  dvds2ln  15642  prmgaplem5  16391  prmgaplem8  16394  cshwsidrepsw  16427  ressress  16562  f1ovscpbl  16799  mreexexlem4d  16918  mreexexd  16919  2oppccomf  16995  fthmon  17197  fuccocl  17234  fucidcl  17235  invfuc  17244  initoeu2lem1  17274  curf2cl  17481  yonedalem4c  17527  yonedalem3  17530  pospo  17583  latjle12  17672  latjlej1  17675  latnlej2  17681  latlem12  17688  latmlem1  17691  latledi  17699  latjass  17705  latj12  17706  latj32  17707  latj13  17708  latj31  17709  latjrot  17710  latjjdi  17713  latjjdir  17714  latdisdlem  17799  prdsmndd  17944  imasmnd2  17948  imasmnd  17949  frmdmnd  18024  grpsubadd  18187  grpaddsubass  18189  grpsubsub4  18192  grppnpcan2  18193  grpnpncan  18194  grpnnncan2  18196  imasgrp2  18214  imasgrp  18215  mulgnndir  18256  mulgnn0dir  18257  mulgnnass  18262  mulgnn0ass  18263  mulgass  18264  pwsmulg  18272  issubg2  18294  qusgrp  18335  galcan  18434  gacan  18435  oppgmnd  18482  pmtrprfv  18581  pmtr3ncom  18603  psgnunilem3  18624  frgp0  18886  cmn32  18925  cmn12  18927  abladdsub  18935  ablsubsub23  18945  mulgdi  18947  mulgsubdi  18950  dprdss  19151  dprdf1o  19154  dprdsn  19158  dmdprdsplit  19169  pgpfac1lem5  19201  srgi  19261  ringi  19310  prdsringd  19362  imasring  19369  opprring  19381  mulgass3  19387  dvrass  19440  kerf1ghm  19497  kerf1hrmOLD  19498  subrgunit  19553  issubrg2  19555  abvdiv  19608  lss1  19710  lsssn0  19719  islss3  19731  prdslmodd  19741  islmhm2  19810  lspsolv  19915  lbsextlem4  19933  sralmod  19959  sraassa  20099  psrbaglesupp  20148  psrbagcon  20151  psrgrp  20178  psrlmod  20181  psrring  20191  psrassa  20194  mpllsslem  20215  ipdi  20784  ipsubdir  20786  ipsubdi  20787  ipassr  20790  ipassr2  20791  isphld  20798  ocvlss  20816  mamudm  20999  matring  21052  matassa  21053  ofco2  21060  scmatlss  21134  ma1repveval  21180  mdetunilem1  21221  mdetunilem9  21229  monmatcollpw  21387  iinopn  21510  restopnb  21783  subbascn  21862  hausnei2  21961  nrmsep2  21964  isnrm3  21967  t1sep  21978  regsep2  21984  dnsconst  21986  dfconn2  22027  dislly  22105  tx1stc  22258  qtophmeo  22425  filss  22461  infil  22471  fsubbas  22475  filssufilg  22519  hauspwpwf1  22595  cnextcn  22675  tmdcn2  22697  psmettri  22921  isxmet2d  22937  xmettri  22961  xmetres2  22971  bldisj  23008  blss2ps  23013  blss2  23014  xmstri2  23076  mstri2  23077  xmstri  23078  mstri  23079  xmstri3  23080  mstri3  23081  msrtri  23082  comet  23123  met2ndci  23132  ngprcan  23219  ngplcan  23220  ngpsubcan  23223  nmtri2  23236  nrgdsdi  23274  nrgdsdir  23275  nlmdsdi  23290  nlmdsdir  23291  blcvx  23406  iocopnst  23544  icccvx  23554  pi1grplem  23653  pi1xfrf  23657  pi1cof  23663  clmpm1dir  23707  cmodscmulexp  23726  cvsdiv  23736  cvsdivcl  23737  cphdivcl  23786  cphsubdir  23812  cphsubdi  23813  bcthlem5  23931  rrxcph  23995  volfiniun  24148  volcn  24207  itg1val2  24285  dvconst  24514  dvlip  24590  ftc1a  24634  ulmdvlem3  24990  ang180  25392  cvxcl  25562  scvxcvx  25563  sgmmul  25777  logexprlim  25801  dchrabl  25830  motgrp  26329  iscgra1  26596  cgrane2  26599  cgrane4  26601  cgrahl1  26602  cgrahl2  26603  cgracgr  26604  cgratr  26609  cgrabtwn  26612  cgrahl  26613  dfcgra2  26616  sacgr  26617  f1otrge  26658  xmstrkgc  26672  colinearalglem1  26692  colinearalg  26696  axcgrtr  26701  axlowdimlem16  26743  axeuclidlem  26748  axcontlem4  26753  axcontlem7  26756  axcontlem12  26761  eengtrkg  26772  eengtrkge  26773  edglnl  26928  subgruhgredgd  27066  nbfusgrlevtxm2  27160  upgrwlkdvde  27518  crctcshwlkn0lem5  27592  crctcshwlkn0  27599  umgrwwlks2on  27736  rusgrnumwwlks  27753  clwlkclwwlkfo  27787  3spthd  27955  frgr2wwlkeqm  28110  dlwwlknondlwlknonf1o  28144  numclwwlk5  28167  friendship  28178  grpomuldivass  28318  ablodivdiv4  28331  dipdi  28620  dipsubdi  28626  disjdsct  30438  omndmul2  30713  archiabllem2c  30824  dvrdir  30861  dvrcan5  30864  reofld  30913  eqgvscpbl  30919  qusscaval  30921  quslmod  30923  quslmhm  30924  prmidlc  30964  ssmxidl  30979  drgextlsp  30996  ccfldsrarelvec  31056  pstmfval  31136  qqhval2lem  31222  qqhvq  31228  esumcvg  31345  sigaclcu  31376  measdivcst  31483  measdivcstALTV  31484  carsggect  31576  tgoldbachgtd  31933  bnj970  32219  bnj910  32220  erdszelem9  32446  cvmseu  32523  elmrsubrn  32767  noprefixmo  33202  nosupbnd1  33214  ssltsep  33259  cgrid2  33464  btwncomim  33474  btwnswapid  33478  trisegint  33489  cgrxfr  33516  btwnxfr  33517  brofs2  33538  brifs2  33539  endofsegid  33546  btwnconn1lem11  33558  btwnconn2  33563  segcon2  33566  seglemin  33574  segletr  33575  btwnsegle  33578  colinbtwnle  33579  broutsideof2  33583  btwnoutside  33586  broutsideof3  33587  outsideoftr  33590  outsidele  33593  ellines  33613  linethrueu  33617  unbdqndv2  33850  poimirlem28  34935  ftc1anc  34990  sdclem1  35033  sstotbnd2  35067  ismndo1  35166  zerdivemp1x  35240  isdrngo2  35251  iscringd  35291  lsmsat  36159  lfladdcl  36222  lflnegcl  36226  lflvscl  36228  lshpkrlem4  36264  lshpkrlem6  36266  ldualgrplem  36296  lduallmodlem  36303  latmassOLD  36380  latm12  36381  latm32  36382  latmrot  36383  latmmdiN  36385  latmmdir  36386  omlfh1N  36409  omlfh3N  36410  cvrnbtwn2  36426  cvlexchb1  36481  cvlexch3  36483  cvlexch4N  36484  cvlatexchb1  36485  cvlsupr2  36494  hlatjass  36521  hlatj12  36522  hlatj32  36523  cvrat  36573  atcvrj0  36579  cvrat2  36580  atltcvr  36586  atexchltN  36592  cvrat3  36593  cvrat4  36594  atbtwnexOLDN  36598  atbtwnex  36599  3dimlem3  36612  3dimlem3OLDN  36613  3at  36641  2atneat  36666  llncmp  36673  2at0mat0  36676  2atmat0  36677  islpln2a  36699  llncvrlpln  36709  lplncmp  36713  3atnelvolN  36737  4atlem11  36760  lplncvrlvol  36767  lvolcmp  36768  2atm2atN  36936  elpaddatriN  36954  elpadd2at2  36958  paddasslem8  36978  paddasslem17  36987  paddass  36989  padd12N  36990  paddssw1  36994  pmodlem2  36998  pmodN  37001  pmapjlln1  37006  atmod1i2  37010  pexmidlem2N  37122  pexmidlem7N  37127  pl42lem2N  37131  pl42lem3N  37132  pl42lem4N  37133  pl42N  37134  lhp2lt  37152  lhpm0atN  37180  lautlt  37242  lautcvr  37243  lautj  37244  lautm  37245  ltrneq2  37299  cdleme1b  37377  cdleme3b  37380  cdleme3c  37381  cdleme9b  37403  cdlemefs27cl  37564  cdleme42mN  37638  cdlemg4c  37763  trljco  37891  tgrpgrplem  37900  tendoplass  37934  tendodi1  37935  tendodi2  37936  erngplus2  37955  erngplus2-rN  37963  cdlemk36  38064  erngdvlem3  38141  erngdvlem3-rN  38149  dvaplusgv  38161  tendospass  38170  tendospdi1  38171  dvalveclem  38176  dialss  38197  dvhvaddass  38248  dvhopvsca  38253  dvhlveclem  38259  diblss  38321  diclss  38344  diclspsn  38345  cdlemn11pre  38361  dihmeetlem12N  38469  dihmeetlem16N  38473  dihmeetlem17N  38474  dvh4dimN  38598  lpolsatN  38639  lpolpolsatN  38640  dochpolN  38641  lclkr  38684  lclkrs  38690  lcfr  38736  irrapxlem6  39473  jm2.26lem3  39647  mpaamn  39805  mendring  39841  mendlmod  39842  mendassa  39843  neicvgel1  40518  rfcnpre4  41340  fmuldfeq  41913  stoweidlem43  42377  stoweidlem52  42386  stoweidlem53  42387  stoweidlem56  42390  issmfgt  43082  issmfge  43095  iccelpart  43642  prproropf1olem1  43714  fmtnoprmfac1  43776  fmtnoprmfac2  43778  copissgrp  44124  ringrng  44199  cznrng  44275  funcringcsetcALTV2lem9  44364  funcringcsetclem9ALTV  44387  linccl  44518  lincsumscmcl  44537  ldepsprlem  44576  lincresunit3lem1  44583  itsclc0yqe  44797