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  7086  fpr2g  7151  isopolem  7286  fr3nr  7712  sexp3  8093  suppfnss  8129  naddass  8621  dif1en  9084  elfir  9324  intrnfi  9325  fisupcl  9379  cnfcomlem  9614  ttrclss  9635  dmttrcl  9636  rnttrcl  9637  ttrclselem2  9641  ackbij1lem15  10146  pwfseqlem4a  10574  pwfseqlem4  10575  eluzuzle  12762  xlesubadd  13183  elioc2  13330  elico2  13331  elicc2  13332  fseq1p1m1  13519  ccatswrd  14593  pfxccat3a  14662  2cshw  14737  tanadd  16094  dvds2ln  16218  prmgaplem5  16985  prmgaplem8  16988  cshwsidrepsw  17023  ressress  17176  f1ovscpbl  17448  mreexexlem4d  17571  mreexexd  17572  2oppccomf  17649  fthmon  17854  fuccocl  17892  fucidcl  17893  invfuc  17902  initoeu2lem1  17939  curf2cl  18155  yonedalem4c  18201  yonedalem3  18204  pospo  18267  latjle12  18374  latjlej1  18377  latnlej2  18383  latlem12  18390  latmlem1  18393  latledi  18401  latjass  18407  latj12  18408  latj32  18409  latj13  18410  latj31  18411  latjrot  18412  latjjdi  18415  latjjdir  18416  latdisdlem  18420  prdssgrpd  18625  prdsmndd  18662  imasmnd2  18666  imasmnd  18667  frmdmnd  18751  grpsubadd  18925  grpaddsubass  18927  grpsubsub4  18930  grppnpcan2  18931  grpnpncan  18932  grpnnncan2  18934  imasgrp2  18952  imasgrp  18953  mulgnndir  19000  mulgnn0dir  19001  mulgnnass  19006  mulgnn0ass  19007  mulgass  19008  pwsmulg  19016  issubg2  19038  qusgrp  19083  kerf1ghm  19144  galcan  19201  gacan  19202  oppgmnd  19251  pmtrprfv  19350  pmtr3ncom  19372  psgnunilem3  19393  frgp0  19657  cmn32  19697  cmn12  19699  abladdsub  19709  ablsubaddsub  19711  ablsubsub23  19721  mulgdi  19723  mulgsubdi  19726  dprdss  19928  dprdf1o  19931  dprdsn  19935  dmdprdsplit  19946  pgpfac1lem5  19978  omndmul2  20030  prdsrngd  20079  imasrng  20080  srgdilem  20095  ringdilem  20152  ringrng  20188  prdsringd  20224  imasring  20233  opprrng  20248  mulgass3  20256  dvrass  20311  dvrdir  20315  subrgunit  20493  issubrg2  20495  isdomn4  20619  abvdiv  20732  lss1  20859  lsssn0  20869  islss3  20880  prdslmodd  20890  islmhm2  20960  lspsolv  21068  lbsextlem4  21086  sralmod  21109  rnglidl1  21157  ipdi  21565  ipsubdir  21567  ipsubdi  21568  ipassr  21571  ipassr2  21572  isphld  21579  ocvlss  21597  sraassab  21793  sraassaOLD  21795  psrgrpOLD  21882  psrlmod  21885  psrring  21895  psrassa  21898  mpllsslem  21925  mamudm  22298  matring  22346  matassa  22347  ofco2  22354  scmatlss  22428  ma1repveval  22474  mdetunilem1  22515  mdetunilem9  22523  monmatcollpw  22682  iinopn  22805  restopnb  23078  subbascn  23157  hausnei2  23256  nrmsep2  23259  isnrm3  23262  t1sep  23273  regsep2  23279  dnsconst  23281  dfconn2  23322  dislly  23400  tx1stc  23553  qtophmeo  23720  filss  23756  infil  23766  fsubbas  23770  filssufilg  23814  hauspwpwf1  23890  cnextcn  23970  tmdcn2  23992  psmettri  24215  isxmet2d  24231  xmettri  24255  xmetres2  24265  bldisj  24302  blss2ps  24307  blss2  24308  xmstri2  24370  mstri2  24371  xmstri  24372  mstri  24373  xmstri3  24374  mstri3  24375  msrtri  24376  comet  24417  met2ndci  24426  ngprcan  24514  ngplcan  24515  ngpsubcan  24518  nmtri2  24531  nrgdsdi  24569  nrgdsdir  24570  nlmdsdi  24585  nlmdsdir  24586  blcvx  24702  iocopnst  24853  icccvx  24864  pi1grplem  24965  pi1xfrf  24969  pi1cof  24975  clmpm1dir  25019  cmodscmulexp  25038  cvsdiv  25048  cvsdivcl  25049  cphdivcl  25098  cphsubdir  25124  cphsubdi  25125  bcthlem5  25244  rrxcph  25308  volfiniun  25464  volcn  25523  itg1val2  25601  dvconst  25834  dvlip  25914  ftc1a  25960  ulmdvlem3  26327  ang180  26740  cvxcl  26911  scvxcvx  26912  sgmmul  27128  logexprlim  27152  dchrabl  27181  nosupbnd1  27642  noinfbnd1lem5  27655  noinfbnd1  27657  ssltsep  27719  addscom  27896  addsbday  27947  addsdi  28081  mulsass  28092  motgrp  28506  iscgra1  28773  cgrane2  28776  cgrane4  28778  cgrahl1  28779  cgrahl2  28780  cgracgr  28781  cgratr  28786  cgrabtwn  28789  cgrahl  28790  dfcgra2  28793  sacgr  28794  f1otrge  28835  xmstrkgc  28849  colinearalglem1  28869  colinearalg  28873  axcgrtr  28878  axlowdimlem16  28920  axeuclidlem  28925  axcontlem4  28930  axcontlem7  28933  axcontlem12  28938  eengtrkg  28949  eengtrkge  28950  edglnl  29106  subgruhgredgd  29247  nbfusgrlevtxm2  29341  upgrwlkdvde  29700  crctcshwlkn0lem5  29777  crctcshwlkn0  29784  umgrwwlks2on  29920  rusgrnumwwlks  29937  clwlkclwwlkfo  29971  3spthd  30138  frgr2wwlkeqm  30293  dlwwlknondlwlknonf1o  30327  numclwwlk5  30350  friendship  30361  grpomuldivass  30503  ablodivdiv4  30516  dipdi  30805  dipsubdi  30811  disjdsct  32659  archiabllem2c  33147  dvrcan5  33186  rloccring  33220  reofld  33291  eqgvscpbl  33297  qusvsval  33299  quslmod  33305  quslmhm  33306  prmidlc  33395  ssdifidl  33404  ssmxidl  33421  ply1degltlss  33538  r1plmhm  33551  drgextlsp  33565  ccfldsrarelvec  33642  constrconj  33711  constrfin  33712  constrelextdg2  33713  pstmfval  33862  qqhval2lem  33947  qqhvq  33953  esumcvg  34052  sigaclcu  34083  measdivcst  34190  measdivcstALTV  34191  carsggect  34285  tgoldbachgtd  34629  bnj970  34913  bnj910  34914  erdszelem9  35171  cvmseu  35248  elmrsubrn  35492  r1peuqusdeg1  35615  cgrid2  35976  btwncomim  35986  btwnswapid  35990  trisegint  36001  cgrxfr  36028  btwnxfr  36029  brofs2  36050  brifs2  36051  endofsegid  36058  btwnconn1lem11  36070  btwnconn2  36075  segcon2  36078  seglemin  36086  segletr  36087  btwnsegle  36090  colinbtwnle  36091  broutsideof2  36095  btwnoutside  36098  broutsideof3  36099  outsideoftr  36102  outsidele  36105  ellines  36125  linethrueu  36129  weiunpo  36438  unbdqndv2  36484  poimirlem28  37627  ftc1anc  37680  sdclem1  37722  sstotbnd2  37753  ismndo1  37852  zerdivemp1x  37926  isdrngo2  37937  iscringd  37977  lsmsat  38986  lfladdcl  39049  lflnegcl  39053  lflvscl  39055  lshpkrlem4  39091  lshpkrlem6  39093  ldualgrplem  39123  lduallmodlem  39130  latmassOLD  39207  latm12  39208  latm32  39209  latmrot  39210  latmmdiN  39212  latmmdir  39213  omlfh1N  39236  omlfh3N  39237  cvrnbtwn2  39253  cvlexchb1  39308  cvlexch3  39310  cvlexch4N  39311  cvlatexchb1  39312  cvlsupr2  39321  hlatjass  39348  hlatj12  39349  hlatj32  39350  cvrat  39401  atcvrj0  39407  cvrat2  39408  atltcvr  39414  atexchltN  39420  cvrat3  39421  cvrat4  39422  atbtwnexOLDN  39426  atbtwnex  39427  3dimlem3  39440  3dimlem3OLDN  39441  3at  39469  2atneat  39494  llncmp  39501  2at0mat0  39504  2atmat0  39505  islpln2a  39527  llncvrlpln  39537  lplncmp  39541  3atnelvolN  39565  4atlem11  39588  lplncvrlvol  39595  lvolcmp  39596  2atm2atN  39764  elpaddatriN  39782  elpadd2at2  39786  paddasslem8  39806  paddasslem17  39815  paddass  39817  padd12N  39818  paddssw1  39822  pmodlem2  39826  pmodN  39829  pmapjlln1  39834  atmod1i2  39838  pexmidlem2N  39950  pexmidlem7N  39955  pl42lem2N  39959  pl42lem3N  39960  pl42lem4N  39961  pl42N  39962  lhp2lt  39980  lhpm0atN  40008  lautlt  40070  lautcvr  40071  lautj  40072  lautm  40073  ltrneq2  40127  cdleme1b  40205  cdleme3b  40208  cdleme3c  40209  cdleme9b  40231  cdlemefs27cl  40392  cdleme42mN  40466  cdlemg4c  40591  trljco  40719  tgrpgrplem  40728  tendoplass  40762  tendodi1  40763  tendodi2  40764  erngplus2  40783  erngplus2-rN  40791  cdlemk36  40892  erngdvlem3  40969  erngdvlem3-rN  40977  dvaplusgv  40989  tendospass  40998  tendospdi1  40999  dvalveclem  41004  dialss  41025  dvhvaddass  41076  dvhopvsca  41081  dvhlveclem  41087  diblss  41149  diclss  41172  diclspsn  41173  cdlemn11pre  41189  dihmeetlem12N  41297  dihmeetlem16N  41301  dihmeetlem17N  41302  dvh4dimN  41426  lpolsatN  41467  lpolpolsatN  41468  dochpolN  41469  lclkr  41512  lclkrs  41518  lcfr  41564  lcmineqlem13  42014  aks6d1c1  42089  irrapxlem6  42800  jm2.26lem3  42974  mpaamn  43129  mendring  43161  mendlmod  43162  mendassa  43163  nnoeomeqom  43285  omabs2  43305  neicvgel1  44092  rfcnpre4  45012  fmuldfeq  45565  stoweidlem43  46025  stoweidlem52  46034  stoweidlem53  46035  stoweidlem56  46038  issmfgt  46738  issmfge  46752  iccelpart  47418  prproropf1olem1  47488  fmtnoprmfac1  47550  fmtnoprmfac2  47552  isubgr3stgrlem2  47952  isubgr3stgrlem4  47954  grlimgrtrilem1  47986  copissgrp  48153  cznrng  48246  funcringcsetcALTV2lem9  48283  funcringcsetclem9ALTV  48306  linccl  48400  lincsumscmcl  48419  ldepsprlem  48458  lincresunit3lem1  48465  itsclc0yqe  48747  resipos  48960  topdlat  48989  catprs  48997  endmndlem  49001  idmon  49006  idepi  49007  thincmon  49419  thincepi  49420  functhinclem1  49430  grptcmon  49579  grptcepi  49580