Theorem simpr3 1195

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 1189	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  1258  simpr23  1261  simpr33  1264  simp1r3  1270  simp2r3  1276  simp3r3  1282  3anandis  1470  funopsn  7167  fpr2g  7230  isopolem  7364  fr3nr  7790  sexp3  8176  suppfnss  8212  naddass  8732  dif1en  9198  elfir  9452  intrnfi  9453  fisupcl  9506  cnfcomlem  9736  ttrclss  9757  dmttrcl  9758  rnttrcl  9759  ttrclselem2  9763  ackbij1lem15  10270  pwfseqlem4a  10698  pwfseqlem4  10699  eluzuzle  12884  xlesubadd  13301  elioc2  13446  elico2  13447  elicc2  13448  fseq1p1m1  13634  ccatswrd  14702  pfxccat3a  14772  2cshw  14847  tanadd  16199  dvds2ln  16322  prmgaplem5  17088  prmgaplem8  17091  cshwsidrepsw  17127  ressress  17293  f1ovscpbl  17572  mreexexlem4d  17691  mreexexd  17692  2oppccomf  17771  fthmon  17980  fuccocl  18020  fucidcl  18021  invfuc  18030  initoeu2lem1  18067  curf2cl  18287  yonedalem4c  18333  yonedalem3  18336  pospo  18402  latjle12  18507  latjlej1  18510  latnlej2  18516  latlem12  18523  latmlem1  18526  latledi  18534  latjass  18540  latj12  18541  latj32  18542  latj13  18543  latj31  18544  latjrot  18545  latjjdi  18548  latjjdir  18549  latdisdlem  18553  prdssgrpd  18758  prdsmndd  18795  imasmnd2  18799  imasmnd  18800  frmdmnd  18884  grpsubadd  19058  grpaddsubass  19060  grpsubsub4  19063  grppnpcan2  19064  grpnpncan  19065  grpnnncan2  19067  imasgrp2  19085  imasgrp  19086  mulgnndir  19133  mulgnn0dir  19134  mulgnnass  19139  mulgnn0ass  19140  mulgass  19141  pwsmulg  19149  issubg2  19171  qusgrp  19216  kerf1ghm  19277  galcan  19334  gacan  19335  oppgmnd  19387  pmtrprfv  19485  pmtr3ncom  19507  psgnunilem3  19528  frgp0  19792  cmn32  19832  cmn12  19834  abladdsub  19844  ablsubaddsub  19846  ablsubsub23  19856  mulgdi  19858  mulgsubdi  19861  dprdss  20063  dprdf1o  20066  dprdsn  20070  dmdprdsplit  20081  pgpfac1lem5  20113  prdsrngd  20193  imasrng  20194  srgdilem  20209  ringdilem  20266  ringrng  20298  prdsringd  20334  imasring  20343  opprrng  20361  mulgass3  20369  dvrass  20424  dvrdir  20428  subrgunit  20606  issubrg2  20608  isdomn4  20732  abvdiv  20846  lss1  20953  lsssn0  20963  islss3  20974  prdslmodd  20984  islmhm2  21054  lspsolv  21162  lbsextlem4  21180  sralmod  21211  rnglidl1  21259  ipdi  21675  ipsubdir  21677  ipsubdi  21678  ipassr  21681  ipassr2  21682  isphld  21689  ocvlss  21707  sraassab  21905  sraassaOLD  21907  psrgrpOLD  21994  psrlmod  21997  psrring  22007  psrassa  22010  mpllsslem  22037  mamudm  22414  matring  22464  matassa  22465  ofco2  22472  scmatlss  22546  ma1repveval  22592  mdetunilem1  22633  mdetunilem9  22641  monmatcollpw  22800  iinopn  22923  restopnb  23198  subbascn  23277  hausnei2  23376  nrmsep2  23379  isnrm3  23382  t1sep  23393  regsep2  23399  dnsconst  23401  dfconn2  23442  dislly  23520  tx1stc  23673  qtophmeo  23840  filss  23876  infil  23886  fsubbas  23890  filssufilg  23934  hauspwpwf1  24010  cnextcn  24090  tmdcn2  24112  psmettri  24336  isxmet2d  24352  xmettri  24376  xmetres2  24386  bldisj  24423  blss2ps  24428  blss2  24429  xmstri2  24491  mstri2  24492  xmstri  24493  mstri  24494  xmstri3  24495  mstri3  24496  msrtri  24497  comet  24541  met2ndci  24550  ngprcan  24638  ngplcan  24639  ngpsubcan  24642  nmtri2  24655  nrgdsdi  24701  nrgdsdir  24702  nlmdsdi  24717  nlmdsdir  24718  blcvx  24833  iocopnst  24983  icccvx  24994  pi1grplem  25095  pi1xfrf  25099  pi1cof  25105  clmpm1dir  25149  cmodscmulexp  25168  cvsdiv  25178  cvsdivcl  25179  cphdivcl  25229  cphsubdir  25255  cphsubdi  25256  bcthlem5  25375  rrxcph  25439  volfiniun  25595  volcn  25654  itg1val2  25732  dvconst  25966  dvlip  26046  ftc1a  26092  ulmdvlem3  26459  ang180  26871  cvxcl  27042  scvxcvx  27043  sgmmul  27259  logexprlim  27283  dchrabl  27312  nosupbnd1  27773  noinfbnd1lem5  27786  noinfbnd1  27788  ssltsep  27849  addscom  28013  addsbday  28064  addsdi  28195  mulsass  28206  motgrp  28565  iscgra1  28832  cgrane2  28835  cgrane4  28837  cgrahl1  28838  cgrahl2  28839  cgracgr  28840  cgratr  28845  cgrabtwn  28848  cgrahl  28849  dfcgra2  28852  sacgr  28853  f1otrge  28894  xmstrkgc  28914  colinearalglem1  28935  colinearalg  28939  axcgrtr  28944  axlowdimlem16  28986  axeuclidlem  28991  axcontlem4  28996  axcontlem7  28999  axcontlem12  29004  eengtrkg  29015  eengtrkge  29016  edglnl  29174  subgruhgredgd  29315  nbfusgrlevtxm2  29409  upgrwlkdvde  29769  crctcshwlkn0lem5  29843  crctcshwlkn0  29850  umgrwwlks2on  29986  rusgrnumwwlks  30003  clwlkclwwlkfo  30037  3spthd  30204  frgr2wwlkeqm  30359  dlwwlknondlwlknonf1o  30393  numclwwlk5  30416  friendship  30427  grpomuldivass  30569  ablodivdiv4  30582  dipdi  30871  dipsubdi  30877  disjdsct  32717  omndmul2  33071  archiabllem2c  33184  dvrcan5  33225  rloccring  33256  reofld  33351  eqgvscpbl  33357  qusvsval  33359  quslmod  33365  quslmhm  33366  prmidlc  33455  ssdifidl  33464  ssmxidl  33481  ply1degltlss  33596  r1plmhm  33609  drgextlsp  33622  ccfldsrarelvec  33695  constrconj  33749  constrfin  33750  constrelextdg2  33751  pstmfval  33856  qqhval2lem  33943  qqhvq  33949  esumcvg  34066  sigaclcu  34097  measdivcst  34204  measdivcstALTV  34205  carsggect  34299  tgoldbachgtd  34655  bnj970  34939  bnj910  34940  erdszelem9  35183  cvmseu  35260  elmrsubrn  35504  r1peuqusdeg1  35627  cgrid2  35984  btwncomim  35994  btwnswapid  35998  trisegint  36009  cgrxfr  36036  btwnxfr  36037  brofs2  36058  brifs2  36059  endofsegid  36066  btwnconn1lem11  36078  btwnconn2  36083  segcon2  36086  seglemin  36094  segletr  36095  btwnsegle  36098  colinbtwnle  36099  broutsideof2  36103  btwnoutside  36106  broutsideof3  36107  outsideoftr  36110  outsidele  36113  ellines  36133  linethrueu  36137  weiunpo  36447  unbdqndv2  36493  poimirlem28  37634  ftc1anc  37687  sdclem1  37729  sstotbnd2  37760  ismndo1  37859  zerdivemp1x  37933  isdrngo2  37944  iscringd  37984  lsmsat  38989  lfladdcl  39052  lflnegcl  39056  lflvscl  39058  lshpkrlem4  39094  lshpkrlem6  39096  ldualgrplem  39126  lduallmodlem  39133  latmassOLD  39210  latm12  39211  latm32  39212  latmrot  39213  latmmdiN  39215  latmmdir  39216  omlfh1N  39239  omlfh3N  39240  cvrnbtwn2  39256  cvlexchb1  39311  cvlexch3  39313  cvlexch4N  39314  cvlatexchb1  39315  cvlsupr2  39324  hlatjass  39351  hlatj12  39352  hlatj32  39353  cvrat  39404  atcvrj0  39410  cvrat2  39411  atltcvr  39417  atexchltN  39423  cvrat3  39424  cvrat4  39425  atbtwnexOLDN  39429  atbtwnex  39430  3dimlem3  39443  3dimlem3OLDN  39444  3at  39472  2atneat  39497  llncmp  39504  2at0mat0  39507  2atmat0  39508  islpln2a  39530  llncvrlpln  39540  lplncmp  39544  3atnelvolN  39568  4atlem11  39591  lplncvrlvol  39598  lvolcmp  39599  2atm2atN  39767  elpaddatriN  39785  elpadd2at2  39789  paddasslem8  39809  paddasslem17  39818  paddass  39820  padd12N  39821  paddssw1  39825  pmodlem2  39829  pmodN  39832  pmapjlln1  39837  atmod1i2  39841  pexmidlem2N  39953  pexmidlem7N  39958  pl42lem2N  39962  pl42lem3N  39963  pl42lem4N  39964  pl42N  39965  lhp2lt  39983  lhpm0atN  40011  lautlt  40073  lautcvr  40074  lautj  40075  lautm  40076  ltrneq2  40130  cdleme1b  40208  cdleme3b  40211  cdleme3c  40212  cdleme9b  40234  cdlemefs27cl  40395  cdleme42mN  40469  cdlemg4c  40594  trljco  40722  tgrpgrplem  40731  tendoplass  40765  tendodi1  40766  tendodi2  40767  erngplus2  40786  erngplus2-rN  40794  cdlemk36  40895  erngdvlem3  40972  erngdvlem3-rN  40980  dvaplusgv  40992  tendospass  41001  tendospdi1  41002  dvalveclem  41007  dialss  41028  dvhvaddass  41079  dvhopvsca  41084  dvhlveclem  41090  diblss  41152  diclss  41175  diclspsn  41176  cdlemn11pre  41192  dihmeetlem12N  41300  dihmeetlem16N  41304  dihmeetlem17N  41305  dvh4dimN  41429  lpolsatN  41470  lpolpolsatN  41471  dochpolN  41472  lclkr  41515  lclkrs  41521  lcfr  41567  lcmineqlem13  42022  aks6d1c1  42097  irrapxlem6  42814  jm2.26lem3  42989  mpaamn  43144  mendring  43176  mendlmod  43177  mendassa  43178  nnoeomeqom  43301  omabs2  43321  neicvgel1  44108  rfcnpre4  44971  fmuldfeq  45538  stoweidlem43  45998  stoweidlem52  46007  stoweidlem53  46008  stoweidlem56  46011  issmfgt  46711  issmfge  46725  iccelpart  47357  prproropf1olem1  47427  fmtnoprmfac1  47489  fmtnoprmfac2  47491  isubgr3stgrlem2  47869  isubgr3stgrlem4  47871  grlimgrtrilem1  47896  copissgrp  48011  cznrng  48104  funcringcsetcALTV2lem9  48141  funcringcsetclem9ALTV  48164  linccl  48259  lincsumscmcl  48278  ldepsprlem  48317  lincresunit3lem1  48324  itsclc0yqe  48610  topdlat  48792  catprs  48799  endmndlem  48803  idmon  48804  idepi  48805  thincmon  48833  thincepi  48834  functhinclem1  48840  grptcmon  48901  grptcepi  48902