Theorem simpr3 1214

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  simpr13  1277  simpr23  1280  simpr33  1283  simp1r3  1289  simp2r3  1295  simp3r3  1301  3anandis  1499  funopsn  7144  funopsnOLD  7145  fpr2g  7209  isopolem  7343  fr3nr  7769  sexp3  8147  suppfnss  8183  naddass  8681  dif1en  9144  elfir  9373  intrnfi  9374  fisupcl  9428  cnfcomlem  9666  ttrclss  9687  dmttrcl  9688  rnttrcl  9689  ttrclselem2  9693  ackbij1lem15  10223  pwfseqlem4a  10652  pwfseqlem4  10653  eluzuzle  12877  xlesubadd  13295  elioc2  13442  elico2  13443  elicc2  13444  fseq1p1m1  13633  ccatswrd  14713  pfxccat3a  14782  2cshw  14857  tanadd  16229  dvds2ln  16353  prmgaplem5  17121  prmgaplem8  17124  cshwsidrepsw  17159  ressress  17313  f1ovscpbl  17586  mreexexlem4d  17709  mreexexd  17710  2oppccomf  17787  fthmon  17992  fuccocl  18030  fucidcl  18031  invfuc  18040  initoeu2lem1  18077  curf2cl  18293  yonedalem4c  18339  yonedalem3  18342  pospo  18405  latjle12  18512  latjlej1  18515  latnlej2  18521  latlem12  18528  latmlem1  18531  latledi  18539  latjass  18545  latj12  18546  latj32  18547  latj13  18548  latj31  18549  latjrot  18550  latjjdi  18553  latjjdir  18554  latdisdlem  18558  prdssgrpd  18797  prdsmndd  18834  imasmnd2  18838  imasmnd  18839  frmdmnd  18924  grpsubadd  19100  grpaddsubass  19102  grpsubsub4  19105  grppnpcan2  19106  grpnpncan  19107  grpnnncan2  19109  imasgrp2  19127  imasgrp  19128  mulgnndir  19175  mulgnn0dir  19176  mulgnnass  19181  mulgnn0ass  19182  mulgass  19183  pwsmulg  19191  issubg2  19214  qusgrp  19263  kerf1ghm  19323  galcan  19380  gacan  19381  oppgmnd  19430  pmtrprfv  19529  pmtr3ncom  19551  psgnunilem3  19572  frgp0  19836  cmn32  19876  cmn12  19878  abladdsub  19888  ablsubaddsub  19890  ablsubsub23  19900  mulgdi  19902  mulgsubdi  19905  dprdss  20107  dprdf1o  20110  dprdsn  20114  dmdprdsplit  20125  pgpfac1lem5  20157  omndmul2  20209  prdsrngd  20260  imasrng  20261  srgdilem  20280  ringdilem  20337  ringrng  20375  prdsringd  20409  imasring  20419  opprrng  20434  mulgass3  20442  dvrass  20497  dvrdir  20501  subrgunit  20700  issubrg2  20702  isdomn4  20825  abvdiv  20943  lss1  21070  lsssn0  21080  islss3  21091  prdslmodd  21101  islmhm2  21170  lspsolv  21278  lbsextlem4  21296  sralmod  21319  rnglidl1  21369  prmidlc  21484  ssdifidl  21496  ipdi  21801  ipsubdir  21803  ipsubdi  21804  ipassr  21807  ipassr2  21808  isphld  21815  ocvlss  21833  sraassab  22029  psrlmod  22120  psrring  22130  psrassa  22133  mpllsslem  22160  mamudm  22563  matring  22611  matassa  22612  ofco2  22619  scmatlss  22693  ma1repveval  22739  mdetunilem1  22780  mdetunilem9  22788  monmatcollpw  22947  iinopn  23070  restopnb  23343  subbascn  23422  hausnei2  23521  nrmsep2  23524  isnrm3  23527  t1sep  23538  regsep2  23544  dnsconst  23546  dfconn2  23587  dislly  23665  tx1stc  23818  qtophmeo  23985  filss  24021  infil  24031  fsubbas  24035  filssufilg  24079  hauspwpwf1  24155  cnextcn  24235  tmdcn2  24257  psmettri  24479  isxmet2d  24495  xmettri  24519  xmetres2  24529  bldisj  24566  blss2ps  24571  blss2  24572  xmstri2  24634  mstri2  24635  xmstri  24636  mstri  24637  xmstri3  24638  mstri3  24639  msrtri  24640  comet  24681  met2ndci  24690  ngprcan  24778  ngplcan  24779  ngpsubcan  24782  nmtri2  24795  nrgdsdi  24833  nrgdsdir  24834  nlmdsdi  24849  nlmdsdir  24850  blcvx  24966  iocopnst  25110  icccvx  25120  pi1grplem  25219  pi1xfrf  25223  pi1cof  25229  clmpm1dir  25273  cmodscmulexp  25292  cvsdiv  25302  cvsdivcl  25303  cphdivcl  25352  cphsubdir  25378  cphsubdi  25379  bcthlem5  25498  rrxcph  25562  volfiniun  25717  volcn  25776  itg1val2  25854  dvconst  26087  dvlip  26163  ftc1a  26207  ulmdvlem3  26576  ang180  26990  cvxcl  27160  scvxcvx  27161  sgmmul  27376  logexprlim  27400  dchrabl  27429  nosupbnd1  27889  noinfbnd1lem5  27902  noinfbnd1  27904  sltssep  27971  addscom  28170  addbday  28222  addsdi  28359  mulsass  28370  motgrp  28823  iscgra1  29132  cgrane2  29135  cgrane4  29137  cgrahl1  29138  cgrahl2  29139  cgracgr  29140  cgratr  29145  cgrabtwn  29148  cgrahl  29149  dfcgra2  29152  sacgr  29153  f1otrge  29232  xmstrkgc  29246  colinearalglem1  29267  colinearalg  29271  axcgrtr  29276  axlowdimlem16  29318  axeuclidlem  29323  axcontlem4  29328  axcontlem7  29331  axcontlem12  29336  eengtrkg  29347  eengtrkge  29348  edglnl  29504  subgruhgredgd  29645  nbfusgrlevtxm2  29739  upgrwlkdvde  30097  crctcshwlkn0lem5  30174  crctcshwlkn0  30181  usgrwwlks2on  30318  umgrwwlks2on  30319  rusgrnumwwlks  30337  clwlkclwwlkfo  30371  3spthd  30538  frgr2wwlkeqm  30693  dlwwlknondlwlknonf1o  30727  numclwwlk5  30750  friendship  30761  grpomuldivass  30904  ablodivdiv4  30917  dipdi  31206  dipsubdi  31212  disjdsct  33059  archiabllem2c  33524  dvrcan5  33564  rloccring  33600  reofld  33672  eqgvscpbl  33679  qusvsval  33681  quslmod  33687  quslmhm  33688  ssmxidl  33766  ply1degltlss  33895  r1plmhm  33908  drgextlsp  33993  ccfldsrarelvec  34070  constrconj  34144  constrfin  34145  constrelextdg2  34146  pstmfval  34295  qqhval2lem  34380  qqhvq  34386  esumcvg  34485  sigaclcu  34516  measdivcst  34623  measdivcstALTV  34624  carsggect  34717  tgoldbachgtd  35058  bnj970  35344  bnj910  35345  erdszelem9  35699  cvmseu  35776  elmrsubrn  36020  r1peuqusdeg1  36143  cgrid2  36503  btwncomim  36513  btwnswapid  36517  trisegint  36528  cgrxfr  36555  btwnxfr  36556  brofs2  36577  brifs2  36578  endofsegid  36585  btwnconn1lem11  36597  btwnconn2  36602  segcon2  36605  seglemin  36613  segletr  36614  btwnsegle  36617  colinbtwnle  36618  broutsideof2  36622  btwnoutside  36625  broutsideof3  36626  outsideoftr  36629  outsidele  36632  ellines  36652  linethrueu  36656  nmulprop  36690  nadddi  36724  weiunpo  37004  unbdqndv2  37128  poimirlem28  38327  ftc1anc  38380  sdclem1  38422  sstotbnd2  38453  ismndo1  38552  zerdivemp1x  38626  isdrngo2  38637  iscringd  38677  lsmsat  39810  lfladdcl  39873  lflnegcl  39877  lflvscl  39879  lshpkrlem4  39915  lshpkrlem6  39917  ldualgrplem  39947  lduallmodlem  39954  latmassOLD  40031  latm12  40032  latm32  40033  latmrot  40034  latmmdiN  40036  latmmdir  40037  omlfh1N  40060  omlfh3N  40061  cvrnbtwn2  40077  cvlexchb1  40132  cvlexch3  40134  cvlexch4N  40135  cvlatexchb1  40136  cvlsupr2  40145  hlatjass  40172  hlatj12  40173  hlatj32  40174  cvrat  40224  atcvrj0  40230  cvrat2  40231  atltcvr  40237  atexchltN  40243  cvrat3  40244  cvrat4  40245  atbtwnexOLDN  40249  atbtwnex  40250  3dimlem3  40263  3dimlem3OLDN  40264  3at  40292  2atneat  40317  llncmp  40324  2at0mat0  40327  2atmat0  40328  islpln2a  40350  llncvrlpln  40360  lplncmp  40364  3atnelvolN  40388  4atlem11  40411  lplncvrlvol  40418  lvolcmp  40419  2atm2atN  40587  elpaddatriN  40605  elpadd2at2  40609  paddasslem8  40629  paddasslem17  40638  paddass  40640  padd12N  40641  paddssw1  40645  pmodlem2  40649  pmodN  40652  pmapjlln1  40657  atmod1i2  40661  pexmidlem2N  40773  pexmidlem7N  40778  pl42lem2N  40782  pl42lem3N  40783  pl42lem4N  40784  pl42N  40785  lhp2lt  40803  lhpm0atN  40831  lautlt  40893  lautcvr  40894  lautj  40895  lautm  40896  ltrneq2  40950  cdleme1b  41028  cdleme3b  41031  cdleme3c  41032  cdleme9b  41054  cdlemefs27cl  41215  cdleme42mN  41289  cdlemg4c  41414  trljco  41542  tgrpgrplem  41551  tendoplass  41585  tendodi1  41586  tendodi2  41587  erngplus2  41606  erngplus2-rN  41614  cdlemk36  41715  erngdvlem3  41792  erngdvlem3-rN  41800  dvaplusgv  41812  tendospass  41821  tendospdi1  41822  dvalveclem  41827  dialss  41848  dvhvaddass  41899  dvhopvsca  41904  dvhlveclem  41910  diblss  41972  diclss  41995  diclspsn  41996  cdlemn11pre  42012  dihmeetlem12N  42120  dihmeetlem16N  42124  dihmeetlem17N  42125  dvh4dimN  42249  lpolsatN  42290  lpolpolsatN  42291  dochpolN  42292  lclkr  42335  lclkrs  42341  lcfr  42387  lcmineqlem13  42836  aks6d1c1  42911  irrapxlem6  43582  jm2.26lem3  43756  mpaamn  43911  mendring  43943  mendlmod  43944  mendassa  43945  nnoeomeqom  44067  omabs2  44087  neicvgel1  44873  rfcnpre4  45782  fmuldfeq  46327  stoweidlem43  46785  stoweidlem52  46794  stoweidlem53  46795  stoweidlem56  46798  issmfgt  47498  issmfge  47512  iccelpart  48210  prproropf1olem1  48280  fmtnoprmfac1  48345  fmtnoprmfac2  48347  isubgr3stgrlem2  48760  isubgr3stgrlem4  48762  grlimgrtrilem1  48794  copissgrp  48961  cznrng  49054  funcringcsetcALTV2lem9  49091  funcringcsetclem9ALTV  49114  idomcanl  49140  linccl  49222  lincsumscmcl  49241  ldepsprlem  49280  lincresunit3lem1  49287  itsclc0yqe  49569  resipos  49781  topdlat  49810  catprs  49817  endmndlem  49821  idmon  49826  idepi  49827  thincmon  50239  thincepi  50240  functhinclem1  50250  grptcmon  50399  grptcepi  50400