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  7151  funopsnOLD  7152  fpr2g  7216  isopolem  7354  fr3nr  7780  sexp3  8158  suppfnss  8194  naddass  8692  dif1en  9156  elfir  9385  intrnfi  9386  fisupcl  9440  cnfcomlem  9678  ttrclss  9699  dmttrcl  9700  rnttrcl  9701  ttrclselem2  9705  ackbij1lem15  10235  pwfseqlem4a  10664  pwfseqlem4  10665  eluzuzle  12889  xlesubadd  13307  elioc2  13454  elico2  13455  elicc2  13456  fseq1p1m1  13645  ccatswrd  14730  pfxccat3a  14799  2cshw  14876  tanadd  16248  dvds2ln  16372  prmgaplem5  17140  prmgaplem8  17143  cshwsidrepsw  17178  ressress  17332  f1ovscpbl  17605  mreexexlem4d  17728  mreexexd  17729  2oppccomf  17806  fthmon  18011  fuccocl  18049  fucidcl  18050  invfuc  18059  initoeu2lem1  18096  curf2cl  18312  yonedalem4c  18358  yonedalem3  18361  pospo  18424  latjle12  18531  latjlej1  18534  latnlej2  18540  latlem12  18547  latmlem1  18550  latledi  18558  latjass  18564  latj12  18565  latj32  18566  latj13  18567  latj31  18568  latjrot  18569  latjjdi  18572  latjjdir  18573  latdisdlem  18577  prdssgrpd  18820  prdsmndd  18859  imasmnd2  18863  imasmnd  18864  frmdmnd  18949  grpsubadd  19125  grpaddsubass  19127  grpsubsub4  19130  grppnpcan2  19131  grpnpncan  19132  grpnnncan2  19134  imasgrp2  19152  imasgrp  19153  mulgnndir  19200  mulgnn0dir  19201  mulgnnass  19206  mulgnn0ass  19207  mulgass  19208  pwsmulg  19216  issubg2  19239  qusgrp  19288  kerf1ghm  19348  galcan  19405  gacan  19406  oppgmnd  19455  pmtrprfv  19554  pmtr3ncom  19576  psgnunilem3  19597  frgp0  19861  cmn32  19901  cmn12  19903  abladdsub  19913  ablsubaddsub  19915  ablsubsub23  19925  mulgdi  19927  mulgsubdi  19930  dprdss  20132  dprdf1o  20135  dprdsn  20139  dmdprdsplit  20150  pgpfac1lem5  20182  omndmul2  20234  prdsrngd  20285  imasrng  20286  srgdilem  20305  ringdilem  20362  ringrng  20400  prdsringd  20435  imasring  20445  opprrng  20460  mulgass3  20468  dvrass  20523  dvrdir  20527  subrgunit  20726  issubrg2  20728  isdomn4  20851  abvdiv  20969  lss1  21096  lsssn0  21106  islss3  21117  prdslmodd  21127  islmhm2  21196  lspsolv  21304  lbsextlem4  21322  sralmod  21345  rnglidl1  21395  prmidlc  21510  ssdifidl  21522  ipdi  21827  ipsubdir  21829  ipsubdi  21830  ipassr  21833  ipassr2  21834  isphld  21841  ocvlss  21859  sraassab  22055  psrlmod  22146  psrring  22156  psrassa  22159  mpllsslem  22186  mamudm  22589  matring  22637  matassa  22638  ofco2  22645  scmatlss  22719  ma1repveval  22765  mdetunilem1  22806  mdetunilem9  22814  monmatcollpw  22973  iinopn  23096  restopnb  23369  subbascn  23448  hausnei2  23547  nrmsep2  23550  isnrm3  23553  t1sep  23564  regsep2  23570  dnsconst  23572  dfconn2  23613  dislly  23691  tx1stc  23844  qtophmeo  24011  filss  24047  infil  24057  fsubbas  24061  filssufilg  24105  hauspwpwf1  24181  cnextcn  24261  tmdcn2  24283  psmettri  24505  isxmet2d  24521  xmettri  24545  xmetres2  24555  bldisj  24592  blss2ps  24597  blss2  24598  xmstri2  24660  mstri2  24661  xmstri  24662  mstri  24663  xmstri3  24664  mstri3  24665  msrtri  24666  comet  24707  met2ndci  24716  ngprcan  24804  ngplcan  24805  ngpsubcan  24808  nmtri2  24821  nrgdsdi  24859  nrgdsdir  24860  nlmdsdi  24875  nlmdsdir  24876  blcvx  24992  iocopnst  25136  icccvx  25146  pi1grplem  25245  pi1xfrf  25249  pi1cof  25255  clmpm1dir  25299  cmodscmulexp  25318  cvsdiv  25328  cvsdivcl  25329  cphdivcl  25378  cphsubdir  25404  cphsubdi  25405  bcthlem5  25524  rrxcph  25588  volfiniun  25743  volcn  25802  itg1val2  25880  dvconst  26113  dvlip  26189  ftc1a  26233  ulmdvlem3  26602  ang180  27016  cvxcl  27186  scvxcvx  27187  sgmmul  27402  logexprlim  27426  dchrabl  27455  nosupbnd1  27915  noinfbnd1lem5  27928  noinfbnd1  27930  sltssep  27997  addscom  28196  addbday  28248  addsdi  28385  mulsass  28396  motgrp  28849  iscgra1  29158  cgrane2  29161  cgrane4  29163  cgrahl1  29164  cgrahl2  29165  cgracgr  29166  cgratr  29171  cgrabtwn  29174  cgrahl  29175  dfcgra2  29178  sacgr  29179  f1otrge  29258  xmstrkgc  29272  colinearalglem1  29293  colinearalg  29297  axcgrtr  29302  axlowdimlem16  29344  axeuclidlem  29349  axcontlem4  29354  axcontlem7  29357  axcontlem12  29362  eengtrkg  29373  eengtrkge  29374  edglnl  29530  subgruhgredgd  29671  nbfusgrlevtxm2  29765  upgrwlkdvde  30123  crctcshwlkn0lem5  30200  crctcshwlkn0  30207  usgrwwlks2on  30344  umgrwwlks2on  30345  rusgrnumwwlks  30363  clwlkclwwlkfo  30397  3spthd  30564  frgr2wwlkeqm  30719  dlwwlknondlwlknonf1o  30753  numclwwlk5  30776  friendship  30787  grpomuldivass  30930  ablodivdiv4  30943  dipdi  31232  dipsubdi  31238  disjdsct  33085  archiabllem2c  33546  dvrcan5  33586  rloccring  33622  reofld  33694  eqgvscpbl  33701  qusvsval  33703  quslmod  33709  quslmhm  33710  ssmxidl  33788  ply1degltlss  33917  r1plmhm  33930  drgextlsp  34015  ccfldsrarelvec  34092  constrconj  34166  constrfin  34167  constrelextdg2  34168  pstmfval  34317  qqhval2lem  34402  qqhvq  34408  esumcvg  34507  sigaclcu  34538  measdivcst  34645  measdivcstALTV  34646  carsggect  34739  tgoldbachgtd  35080  bnj970  35366  bnj910  35367  erdszelem9  35711  cvmseu  35788  elmrsubrn  36032  r1peuqusdeg1  36155  cgrid2  36515  btwncomim  36525  btwnswapid  36529  trisegint  36540  cgrxfr  36567  btwnxfr  36568  brofs2  36589  brifs2  36590  endofsegid  36597  btwnconn1lem11  36609  btwnconn2  36614  segcon2  36617  seglemin  36625  segletr  36626  btwnsegle  36629  colinbtwnle  36630  broutsideof2  36634  btwnoutside  36637  broutsideof3  36638  outsideoftr  36641  outsidele  36644  ellines  36664  linethrueu  36668  nmulprop  36702  nadddi  36736  weiunpo  37016  unbdqndv2  37140  poimirlem28  38339  ftc1anc  38392  sdclem1  38434  sstotbnd2  38465  ismndo1  38564  zerdivemp1x  38638  isdrngo2  38649  iscringd  38689  lsmsat  39822  lfladdcl  39885  lflnegcl  39889  lflvscl  39891  lshpkrlem4  39927  lshpkrlem6  39929  ldualgrplem  39959  lduallmodlem  39966  latmassOLD  40043  latm12  40044  latm32  40045  latmrot  40046  latmmdiN  40048  latmmdir  40049  omlfh1N  40072  omlfh3N  40073  cvrnbtwn2  40089  cvlexchb1  40144  cvlexch3  40146  cvlexch4N  40147  cvlatexchb1  40148  cvlsupr2  40157  hlatjass  40184  hlatj12  40185  hlatj32  40186  cvrat  40236  atcvrj0  40242  cvrat2  40243  atltcvr  40249  atexchltN  40255  cvrat3  40256  cvrat4  40257  atbtwnexOLDN  40261  atbtwnex  40262  3dimlem3  40275  3dimlem3OLDN  40276  3at  40304  2atneat  40329  llncmp  40336  2at0mat0  40339  2atmat0  40340  islpln2a  40362  llncvrlpln  40372  lplncmp  40376  3atnelvolN  40400  4atlem11  40423  lplncvrlvol  40430  lvolcmp  40431  2atm2atN  40599  elpaddatriN  40617  elpadd2at2  40621  paddasslem8  40641  paddasslem17  40650  paddass  40652  padd12N  40653  paddssw1  40657  pmodlem2  40661  pmodN  40664  pmapjlln1  40669  atmod1i2  40673  pexmidlem2N  40785  pexmidlem7N  40790  pl42lem2N  40794  pl42lem3N  40795  pl42lem4N  40796  pl42N  40797  lhp2lt  40815  lhpm0atN  40843  lautlt  40905  lautcvr  40906  lautj  40907  lautm  40908  ltrneq2  40962  cdleme1b  41040  cdleme3b  41043  cdleme3c  41044  cdleme9b  41066  cdlemefs27cl  41227  cdleme42mN  41301  cdlemg4c  41426  trljco  41554  tgrpgrplem  41563  tendoplass  41597  tendodi1  41598  tendodi2  41599  erngplus2  41618  erngplus2-rN  41626  cdlemk36  41727  erngdvlem3  41804  erngdvlem3-rN  41812  dvaplusgv  41824  tendospass  41833  tendospdi1  41834  dvalveclem  41839  dialss  41860  dvhvaddass  41911  dvhopvsca  41916  dvhlveclem  41922  diblss  41984  diclss  42007  diclspsn  42008  cdlemn11pre  42024  dihmeetlem12N  42132  dihmeetlem16N  42136  dihmeetlem17N  42137  dvh4dimN  42261  lpolsatN  42302  lpolpolsatN  42303  dochpolN  42304  lclkr  42347  lclkrs  42353  lcfr  42399  lcmineqlem13  42848  aks6d1c1  42923  irrapxlem6  43594  jm2.26lem3  43768  mpaamn  43923  mendring  43955  mendlmod  43956  mendassa  43957  nnoeomeqom  44079  omabs2  44099  neicvgel1  44885  rfcnpre4  45794  fmuldfeq  46339  stoweidlem43  46797  stoweidlem52  46806  stoweidlem53  46807  stoweidlem56  46810  issmfgt  47510  issmfge  47524  iccelpart  48222  prproropf1olem1  48292  fmtnoprmfac1  48357  fmtnoprmfac2  48359  isubgr3stgrlem2  48772  isubgr3stgrlem4  48774  grlimgrtrilem1  48806  copissgrp  48973  cznrng  49066  funcringcsetcALTV2lem9  49103  funcringcsetclem9ALTV  49126  idomcanl  49152  linccl  49234  lincsumscmcl  49253  ldepsprlem  49292  lincresunit3lem1  49299  itsclc0yqe  49581  resipos  49793  topdlat  49822  catprs  49829  endmndlem  49833  idmon  49838  idepi  49839  thincmon  50251  thincepi  50252  functhinclem1  50262  grptcmon  50411  grptcepi  50412