Theorem simpr3 1213

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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

This theorem is referenced by:  simpr13  1276  simpr23  1279  simpr33  1282  simp1r3  1288  simp2r3  1294  simp3r3  1300  3anandis  1495  funopsn  7134  funopsnOLD  7135  fpr2g  7199  isopolem  7333  fr3nr  7759  sexp3  8137  suppfnss  8173  naddass  8671  dif1en  9134  elfir  9363  intrnfi  9364  fisupcl  9418  cnfcomlem  9656  ttrclss  9677  dmttrcl  9678  rnttrcl  9679  ttrclselem2  9683  ackbij1lem15  10204  pwfseqlem4a  10634  pwfseqlem4  10635  eluzuzle  12862  xlesubadd  13280  elioc2  13427  elico2  13428  elicc2  13429  fseq1p1m1  13617  ccatswrd  14696  pfxccat3a  14765  2cshw  14840  tanadd  16213  dvds2ln  16337  prmgaplem5  17105  prmgaplem8  17108  cshwsidrepsw  17143  ressress  17297  f1ovscpbl  17570  mreexexlem4d  17693  mreexexd  17694  2oppccomf  17771  fthmon  17976  fuccocl  18014  fucidcl  18015  invfuc  18024  initoeu2lem1  18061  curf2cl  18277  yonedalem4c  18323  yonedalem3  18326  pospo  18389  latjle12  18496  latjlej1  18499  latnlej2  18505  latlem12  18512  latmlem1  18515  latledi  18523  latjass  18529  latj12  18530  latj32  18531  latj13  18532  latj31  18533  latjrot  18534  latjjdi  18537  latjjdir  18538  latdisdlem  18542  prdssgrpd  18781  prdsmndd  18818  imasmnd2  18822  imasmnd  18823  frmdmnd  18908  grpsubadd  19085  grpaddsubass  19087  grpsubsub4  19090  grppnpcan2  19091  grpnpncan  19092  grpnnncan2  19094  imasgrp2  19112  imasgrp  19113  mulgnndir  19160  mulgnn0dir  19161  mulgnnass  19166  mulgnn0ass  19167  mulgass  19168  pwsmulg  19176  issubg2  19199  qusgrp  19248  kerf1ghm  19308  galcan  19365  gacan  19366  oppgmnd  19415  pmtrprfv  19514  pmtr3ncom  19536  psgnunilem3  19557  frgp0  19821  cmn32  19861  cmn12  19863  abladdsub  19873  ablsubaddsub  19875  ablsubsub23  19885  mulgdi  19887  mulgsubdi  19890  dprdss  20092  dprdf1o  20095  dprdsn  20099  dmdprdsplit  20110  pgpfac1lem5  20142  omndmul2  20194  prdsrngd  20245  imasrng  20246  srgdilem  20265  ringdilem  20322  ringrng  20359  prdsringd  20393  imasring  20403  opprrng  20418  mulgass3  20426  dvrass  20481  dvrdir  20485  subrgunit  20666  issubrg2  20668  isdomn4  20791  abvdiv  20901  lss1  21028  lsssn0  21038  islss3  21049  prdslmodd  21059  islmhm2  21128  lspsolv  21236  lbsextlem4  21254  sralmod  21277  rnglidl1  21327  prmidlc  21435  ssdifidl  21445  ipdi  21750  ipsubdir  21752  ipsubdi  21753  ipassr  21756  ipassr2  21757  isphld  21764  ocvlss  21782  sraassab  21978  psrlmod  22069  psrring  22079  psrassa  22082  mpllsslem  22109  mamudm  22513  matring  22561  matassa  22562  ofco2  22569  scmatlss  22643  ma1repveval  22689  mdetunilem1  22730  mdetunilem9  22738  monmatcollpw  22897  iinopn  23020  restopnb  23293  subbascn  23372  hausnei2  23471  nrmsep2  23474  isnrm3  23477  t1sep  23488  regsep2  23494  dnsconst  23496  dfconn2  23537  dislly  23615  tx1stc  23768  qtophmeo  23935  filss  23971  infil  23981  fsubbas  23985  filssufilg  24029  hauspwpwf1  24105  cnextcn  24185  tmdcn2  24207  psmettri  24429  isxmet2d  24445  xmettri  24469  xmetres2  24479  bldisj  24516  blss2ps  24521  blss2  24522  xmstri2  24584  mstri2  24585  xmstri  24586  mstri  24587  xmstri3  24588  mstri3  24589  msrtri  24590  comet  24631  met2ndci  24640  ngprcan  24728  ngplcan  24729  ngpsubcan  24732  nmtri2  24745  nrgdsdi  24783  nrgdsdir  24784  nlmdsdi  24799  nlmdsdir  24800  blcvx  24916  iocopnst  25060  icccvx  25070  pi1grplem  25169  pi1xfrf  25173  pi1cof  25179  clmpm1dir  25223  cmodscmulexp  25242  cvsdiv  25252  cvsdivcl  25253  cphdivcl  25302  cphsubdir  25328  cphsubdi  25329  bcthlem5  25448  rrxcph  25512  volfiniun  25667  volcn  25726  itg1val2  25804  dvconst  26037  dvlip  26113  ftc1a  26157  ulmdvlem3  26523  ang180  26937  cvxcl  27107  scvxcvx  27108  sgmmul  27323  logexprlim  27347  dchrabl  27376  nosupbnd1  27836  noinfbnd1lem5  27849  noinfbnd1  27851  sltssep  27918  addscom  28117  addbday  28169  addsdi  28306  mulsass  28317  motgrp  28770  iscgra1  29062  cgrane2  29065  cgrane4  29067  cgrahl1  29068  cgrahl2  29069  cgracgr  29070  cgratr  29075  cgrabtwn  29078  cgrahl  29079  dfcgra2  29082  sacgr  29083  f1otrge  29130  xmstrkgc  29144  colinearalglem1  29165  colinearalg  29169  axcgrtr  29174  axlowdimlem16  29216  axeuclidlem  29221  axcontlem4  29226  axcontlem7  29229  axcontlem12  29234  eengtrkg  29245  eengtrkge  29246  edglnl  29402  subgruhgredgd  29543  nbfusgrlevtxm2  29637  upgrwlkdvde  29995  crctcshwlkn0lem5  30072  crctcshwlkn0  30079  usgrwwlks2on  30216  umgrwwlks2on  30217  rusgrnumwwlks  30235  clwlkclwwlkfo  30269  3spthd  30436  frgr2wwlkeqm  30591  dlwwlknondlwlknonf1o  30625  numclwwlk5  30648  friendship  30659  grpomuldivass  30802  ablodivdiv4  30815  dipdi  31104  dipsubdi  31110  disjdsct  32960  archiabllem2c  33428  dvrcan5  33468  rloccring  33504  reofld  33578  eqgvscpbl  33585  qusvsval  33587  quslmod  33593  quslmhm  33594  ssmxidl  33674  ply1degltlss  33803  r1plmhm  33816  drgextlsp  33901  ccfldsrarelvec  33978  constrconj  34052  constrfin  34053  constrelextdg2  34054  pstmfval  34203  qqhval2lem  34288  qqhvq  34294  esumcvg  34393  sigaclcu  34424  measdivcst  34531  measdivcstALTV  34532  carsggect  34625  tgoldbachgtd  34966  bnj970  35252  bnj910  35253  erdszelem9  35562  cvmseu  35639  elmrsubrn  35883  r1peuqusdeg1  36006  cgrid2  36366  btwncomim  36376  btwnswapid  36380  trisegint  36391  cgrxfr  36418  btwnxfr  36419  brofs2  36440  brifs2  36441  endofsegid  36448  btwnconn1lem11  36460  btwnconn2  36465  segcon2  36468  seglemin  36476  segletr  36477  btwnsegle  36480  colinbtwnle  36481  broutsideof2  36485  btwnoutside  36488  broutsideof3  36489  outsideoftr  36492  outsidele  36495  ellines  36515  linethrueu  36519  nmulprop  36553  weiunpo  36838  unbdqndv2  36962  poimirlem28  38159  ftc1anc  38212  sdclem1  38254  sstotbnd2  38285  ismndo1  38384  zerdivemp1x  38458  isdrngo2  38469  iscringd  38509  lsmsat  39644  lfladdcl  39707  lflnegcl  39711  lflvscl  39713  lshpkrlem4  39749  lshpkrlem6  39751  ldualgrplem  39781  lduallmodlem  39788  latmassOLD  39865  latm12  39866  latm32  39867  latmrot  39868  latmmdiN  39870  latmmdir  39871  omlfh1N  39894  omlfh3N  39895  cvrnbtwn2  39911  cvlexchb1  39966  cvlexch3  39968  cvlexch4N  39969  cvlatexchb1  39970  cvlsupr2  39979  hlatjass  40006  hlatj12  40007  hlatj32  40008  cvrat  40058  atcvrj0  40064  cvrat2  40065  atltcvr  40071  atexchltN  40077  cvrat3  40078  cvrat4  40079  atbtwnexOLDN  40083  atbtwnex  40084  3dimlem3  40097  3dimlem3OLDN  40098  3at  40126  2atneat  40151  llncmp  40158  2at0mat0  40161  2atmat0  40162  islpln2a  40184  llncvrlpln  40194  lplncmp  40198  3atnelvolN  40222  4atlem11  40245  lplncvrlvol  40252  lvolcmp  40253  2atm2atN  40421  elpaddatriN  40439  elpadd2at2  40443  paddasslem8  40463  paddasslem17  40472  paddass  40474  padd12N  40475  paddssw1  40479  pmodlem2  40483  pmodN  40486  pmapjlln1  40491  atmod1i2  40495  pexmidlem2N  40607  pexmidlem7N  40612  pl42lem2N  40616  pl42lem3N  40617  pl42lem4N  40618  pl42N  40619  lhp2lt  40637  lhpm0atN  40665  lautlt  40727  lautcvr  40728  lautj  40729  lautm  40730  ltrneq2  40784  cdleme1b  40862  cdleme3b  40865  cdleme3c  40866  cdleme9b  40888  cdlemefs27cl  41049  cdleme42mN  41123  cdlemg4c  41248  trljco  41376  tgrpgrplem  41385  tendoplass  41419  tendodi1  41420  tendodi2  41421  erngplus2  41440  erngplus2-rN  41448  cdlemk36  41549  erngdvlem3  41626  erngdvlem3-rN  41634  dvaplusgv  41646  tendospass  41655  tendospdi1  41656  dvalveclem  41661  dialss  41682  dvhvaddass  41733  dvhopvsca  41738  dvhlveclem  41744  diblss  41806  diclss  41829  diclspsn  41830  cdlemn11pre  41846  dihmeetlem12N  41954  dihmeetlem16N  41958  dihmeetlem17N  41959  dvh4dimN  42083  lpolsatN  42124  lpolpolsatN  42125  dochpolN  42126  lclkr  42169  lclkrs  42175  lcfr  42221  lcmineqlem13  42670  aks6d1c1  42745  irrapxlem6  43416  jm2.26lem3  43590  mpaamn  43745  mendring  43777  mendlmod  43778  mendassa  43779  nnoeomeqom  43901  omabs2  43921  neicvgel1  44707  rfcnpre4  45612  fmuldfeq  46157  stoweidlem43  46615  stoweidlem52  46624  stoweidlem53  46625  stoweidlem56  46628  issmfgt  47328  issmfge  47342  iccelpart  48037  prproropf1olem1  48107  fmtnoprmfac1  48172  fmtnoprmfac2  48174  isubgr3stgrlem2  48587  isubgr3stgrlem4  48589  grlimgrtrilem1  48621  copissgrp  48788  cznrng  48881  funcringcsetcALTV2lem9  48918  funcringcsetclem9ALTV  48941  linccl  49045  lincsumscmcl  49064  ldepsprlem  49103  lincresunit3lem1  49110  itsclc0yqe  49392  resipos  49604  topdlat  49633  catprs  49640  endmndlem  49644  idmon  49649  idepi  49650  thincmon  50062  thincepi  50063  functhinclem1  50073  grptcmon  50222  grptcepi  50223