Theorem simpr3 1197

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 1191	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simpr13  1260  simpr23  1263  simpr33  1266  simp1r3  1272  simp2r3  1278  simp3r3  1284  3anandis  1473  funopsn  7093  fpr2g  7157  isopolem  7291  fr3nr  7717  sexp3  8095  suppfnss  8131  naddass  8624  dif1en  9086  elfir  9318  intrnfi  9319  fisupcl  9373  cnfcomlem  9608  ttrclss  9629  dmttrcl  9630  rnttrcl  9631  ttrclselem2  9635  ackbij1lem15  10143  pwfseqlem4a  10572  pwfseqlem4  10573  eluzuzle  12760  xlesubadd  13178  elioc2  13325  elico2  13326  elicc2  13327  fseq1p1m1  13514  ccatswrd  14592  pfxccat3a  14661  2cshw  14736  tanadd  16092  dvds2ln  16216  prmgaplem5  16983  prmgaplem8  16986  cshwsidrepsw  17021  ressress  17174  f1ovscpbl  17447  mreexexlem4d  17570  mreexexd  17571  2oppccomf  17648  fthmon  17853  fuccocl  17891  fucidcl  17892  invfuc  17901  initoeu2lem1  17938  curf2cl  18154  yonedalem4c  18200  yonedalem3  18203  pospo  18266  latjle12  18373  latjlej1  18376  latnlej2  18382  latlem12  18389  latmlem1  18392  latledi  18400  latjass  18406  latj12  18407  latj32  18408  latj13  18409  latj31  18410  latjrot  18411  latjjdi  18414  latjjdir  18415  latdisdlem  18419  prdssgrpd  18658  prdsmndd  18695  imasmnd2  18699  imasmnd  18700  frmdmnd  18784  grpsubadd  18958  grpaddsubass  18960  grpsubsub4  18963  grppnpcan2  18964  grpnpncan  18965  grpnnncan2  18967  imasgrp2  18985  imasgrp  18986  mulgnndir  19033  mulgnn0dir  19034  mulgnnass  19039  mulgnn0ass  19040  mulgass  19041  pwsmulg  19049  issubg2  19071  qusgrp  19115  kerf1ghm  19176  galcan  19233  gacan  19234  oppgmnd  19283  pmtrprfv  19382  pmtr3ncom  19404  psgnunilem3  19425  frgp0  19689  cmn32  19729  cmn12  19731  abladdsub  19741  ablsubaddsub  19743  ablsubsub23  19753  mulgdi  19755  mulgsubdi  19758  dprdss  19960  dprdf1o  19963  dprdsn  19967  dmdprdsplit  19978  pgpfac1lem5  20010  omndmul2  20062  prdsrngd  20111  imasrng  20112  srgdilem  20127  ringdilem  20184  ringrng  20220  prdsringd  20256  imasring  20266  opprrng  20281  mulgass3  20289  dvrass  20344  dvrdir  20348  subrgunit  20523  issubrg2  20525  isdomn4  20649  abvdiv  20762  lss1  20889  lsssn0  20899  islss3  20910  prdslmodd  20920  islmhm2  20990  lspsolv  21098  lbsextlem4  21116  sralmod  21139  rnglidl1  21187  ipdi  21595  ipsubdir  21597  ipsubdi  21598  ipassr  21601  ipassr2  21602  isphld  21609  ocvlss  21627  sraassab  21823  sraassaOLD  21825  psrlmod  21915  psrring  21925  psrassa  21928  mpllsslem  21955  mamudm  22339  matring  22387  matassa  22388  ofco2  22395  scmatlss  22469  ma1repveval  22515  mdetunilem1  22556  mdetunilem9  22564  monmatcollpw  22723  iinopn  22846  restopnb  23119  subbascn  23198  hausnei2  23297  nrmsep2  23300  isnrm3  23303  t1sep  23314  regsep2  23320  dnsconst  23322  dfconn2  23363  dislly  23441  tx1stc  23594  qtophmeo  23761  filss  23797  infil  23807  fsubbas  23811  filssufilg  23855  hauspwpwf1  23931  cnextcn  24011  tmdcn2  24033  psmettri  24255  isxmet2d  24271  xmettri  24295  xmetres2  24305  bldisj  24342  blss2ps  24347  blss2  24348  xmstri2  24410  mstri2  24411  xmstri  24412  mstri  24413  xmstri3  24414  mstri3  24415  msrtri  24416  comet  24457  met2ndci  24466  ngprcan  24554  ngplcan  24555  ngpsubcan  24558  nmtri2  24571  nrgdsdi  24609  nrgdsdir  24610  nlmdsdi  24625  nlmdsdir  24626  blcvx  24742  iocopnst  24893  icccvx  24904  pi1grplem  25005  pi1xfrf  25009  pi1cof  25015  clmpm1dir  25059  cmodscmulexp  25078  cvsdiv  25088  cvsdivcl  25089  cphdivcl  25138  cphsubdir  25164  cphsubdi  25165  bcthlem5  25284  rrxcph  25348  volfiniun  25504  volcn  25563  itg1val2  25641  dvconst  25874  dvlip  25954  ftc1a  26000  ulmdvlem3  26367  ang180  26780  cvxcl  26951  scvxcvx  26952  sgmmul  27168  logexprlim  27192  dchrabl  27221  nosupbnd1  27682  noinfbnd1lem5  27695  noinfbnd1  27697  sltssep  27763  addscom  27962  addbday  28014  addsdi  28151  mulsass  28162  motgrp  28615  iscgra1  28882  cgrane2  28885  cgrane4  28887  cgrahl1  28888  cgrahl2  28889  cgracgr  28890  cgratr  28895  cgrabtwn  28898  cgrahl  28899  dfcgra2  28902  sacgr  28903  f1otrge  28944  xmstrkgc  28958  colinearalglem1  28979  colinearalg  28983  axcgrtr  28988  axlowdimlem16  29030  axeuclidlem  29035  axcontlem4  29040  axcontlem7  29043  axcontlem12  29048  eengtrkg  29059  eengtrkge  29060  edglnl  29216  subgruhgredgd  29357  nbfusgrlevtxm2  29451  upgrwlkdvde  29810  crctcshwlkn0lem5  29887  crctcshwlkn0  29894  usgrwwlks2on  30031  umgrwwlks2on  30032  rusgrnumwwlks  30050  clwlkclwwlkfo  30084  3spthd  30251  frgr2wwlkeqm  30406  dlwwlknondlwlknonf1o  30440  numclwwlk5  30463  friendship  30474  grpomuldivass  30616  ablodivdiv4  30629  dipdi  30918  dipsubdi  30924  disjdsct  32782  archiabllem2c  33277  dvrcan5  33318  rloccring  33352  reofld  33424  eqgvscpbl  33431  qusvsval  33433  quslmod  33439  quslmhm  33440  prmidlc  33529  ssdifidl  33538  ssmxidl  33555  ply1degltlss  33677  r1plmhm  33691  drgextlsp  33750  ccfldsrarelvec  33828  constrconj  33902  constrfin  33903  constrelextdg2  33904  pstmfval  34053  qqhval2lem  34138  qqhvq  34144  esumcvg  34243  sigaclcu  34274  measdivcst  34381  measdivcstALTV  34382  carsggect  34475  tgoldbachgtd  34819  bnj970  35103  bnj910  35104  erdszelem9  35393  cvmseu  35470  elmrsubrn  35714  r1peuqusdeg1  35837  cgrid2  36197  btwncomim  36207  btwnswapid  36211  trisegint  36222  cgrxfr  36249  btwnxfr  36250  brofs2  36271  brifs2  36272  endofsegid  36279  btwnconn1lem11  36291  btwnconn2  36296  segcon2  36299  seglemin  36307  segletr  36308  btwnsegle  36311  colinbtwnle  36312  broutsideof2  36316  btwnoutside  36319  broutsideof3  36320  outsideoftr  36323  outsidele  36326  ellines  36346  linethrueu  36350  weiunpo  36659  unbdqndv2  36711  poimirlem28  37845  ftc1anc  37898  sdclem1  37940  sstotbnd2  37971  ismndo1  38070  zerdivemp1x  38144  isdrngo2  38155  iscringd  38195  lsmsat  39264  lfladdcl  39327  lflnegcl  39331  lflvscl  39333  lshpkrlem4  39369  lshpkrlem6  39371  ldualgrplem  39401  lduallmodlem  39408  latmassOLD  39485  latm12  39486  latm32  39487  latmrot  39488  latmmdiN  39490  latmmdir  39491  omlfh1N  39514  omlfh3N  39515  cvrnbtwn2  39531  cvlexchb1  39586  cvlexch3  39588  cvlexch4N  39589  cvlatexchb1  39590  cvlsupr2  39599  hlatjass  39626  hlatj12  39627  hlatj32  39628  cvrat  39678  atcvrj0  39684  cvrat2  39685  atltcvr  39691  atexchltN  39697  cvrat3  39698  cvrat4  39699  atbtwnexOLDN  39703  atbtwnex  39704  3dimlem3  39717  3dimlem3OLDN  39718  3at  39746  2atneat  39771  llncmp  39778  2at0mat0  39781  2atmat0  39782  islpln2a  39804  llncvrlpln  39814  lplncmp  39818  3atnelvolN  39842  4atlem11  39865  lplncvrlvol  39872  lvolcmp  39873  2atm2atN  40041  elpaddatriN  40059  elpadd2at2  40063  paddasslem8  40083  paddasslem17  40092  paddass  40094  padd12N  40095  paddssw1  40099  pmodlem2  40103  pmodN  40106  pmapjlln1  40111  atmod1i2  40115  pexmidlem2N  40227  pexmidlem7N  40232  pl42lem2N  40236  pl42lem3N  40237  pl42lem4N  40238  pl42N  40239  lhp2lt  40257  lhpm0atN  40285  lautlt  40347  lautcvr  40348  lautj  40349  lautm  40350  ltrneq2  40404  cdleme1b  40482  cdleme3b  40485  cdleme3c  40486  cdleme9b  40508  cdlemefs27cl  40669  cdleme42mN  40743  cdlemg4c  40868  trljco  40996  tgrpgrplem  41005  tendoplass  41039  tendodi1  41040  tendodi2  41041  erngplus2  41060  erngplus2-rN  41068  cdlemk36  41169  erngdvlem3  41246  erngdvlem3-rN  41254  dvaplusgv  41266  tendospass  41275  tendospdi1  41276  dvalveclem  41281  dialss  41302  dvhvaddass  41353  dvhopvsca  41358  dvhlveclem  41364  diblss  41426  diclss  41449  diclspsn  41450  cdlemn11pre  41466  dihmeetlem12N  41574  dihmeetlem16N  41578  dihmeetlem17N  41579  dvh4dimN  41703  lpolsatN  41744  lpolpolsatN  41745  dochpolN  41746  lclkr  41789  lclkrs  41795  lcfr  41841  lcmineqlem13  42291  aks6d1c1  42366  irrapxlem6  43065  jm2.26lem3  43239  mpaamn  43394  mendring  43426  mendlmod  43427  mendassa  43428  nnoeomeqom  43550  omabs2  43570  neicvgel1  44356  rfcnpre4  45275  fmuldfeq  45825  stoweidlem43  46283  stoweidlem52  46292  stoweidlem53  46293  stoweidlem56  46296  issmfgt  46996  issmfge  47010  iccelpart  47675  prproropf1olem1  47745  fmtnoprmfac1  47807  fmtnoprmfac2  47809  isubgr3stgrlem2  48209  isubgr3stgrlem4  48211  grlimgrtrilem1  48243  copissgrp  48410  cznrng  48503  funcringcsetcALTV2lem9  48540  funcringcsetclem9ALTV  48563  linccl  48656  lincsumscmcl  48675  ldepsprlem  48714  lincresunit3lem1  48721  itsclc0yqe  49003  resipos  49216  topdlat  49245  catprs  49252  endmndlem  49256  idmon  49261  idepi  49262  thincmon  49674  thincepi  49675  functhinclem1  49685  grptcmon  49834  grptcepi  49835