Theorem simpr3 1198

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  simpr13  1261  simpr23  1264  simpr33  1267  simp1r3  1273  simp2r3  1279  simp3r3  1285  3anandis  1474  funopsn  7103  fpr2g  7167  isopolem  7301  fr3nr  7727  sexp3  8105  suppfnss  8141  naddass  8634  dif1en  9098  elfir  9330  intrnfi  9331  fisupcl  9385  cnfcomlem  9620  ttrclss  9641  dmttrcl  9642  rnttrcl  9643  ttrclselem2  9647  ackbij1lem15  10155  pwfseqlem4a  10584  pwfseqlem4  10585  eluzuzle  12772  xlesubadd  13190  elioc2  13337  elico2  13338  elicc2  13339  fseq1p1m1  13526  ccatswrd  14604  pfxccat3a  14673  2cshw  14748  tanadd  16104  dvds2ln  16228  prmgaplem5  16995  prmgaplem8  16998  cshwsidrepsw  17033  ressress  17186  f1ovscpbl  17459  mreexexlem4d  17582  mreexexd  17583  2oppccomf  17660  fthmon  17865  fuccocl  17903  fucidcl  17904  invfuc  17913  initoeu2lem1  17950  curf2cl  18166  yonedalem4c  18212  yonedalem3  18215  pospo  18278  latjle12  18385  latjlej1  18388  latnlej2  18394  latlem12  18401  latmlem1  18404  latledi  18412  latjass  18418  latj12  18419  latj32  18420  latj13  18421  latj31  18422  latjrot  18423  latjjdi  18426  latjjdir  18427  latdisdlem  18431  prdssgrpd  18670  prdsmndd  18707  imasmnd2  18711  imasmnd  18712  frmdmnd  18796  grpsubadd  18970  grpaddsubass  18972  grpsubsub4  18975  grppnpcan2  18976  grpnpncan  18977  grpnnncan2  18979  imasgrp2  18997  imasgrp  18998  mulgnndir  19045  mulgnn0dir  19046  mulgnnass  19051  mulgnn0ass  19052  mulgass  19053  pwsmulg  19061  issubg2  19083  qusgrp  19127  kerf1ghm  19188  galcan  19245  gacan  19246  oppgmnd  19295  pmtrprfv  19394  pmtr3ncom  19416  psgnunilem3  19437  frgp0  19701  cmn32  19741  cmn12  19743  abladdsub  19753  ablsubaddsub  19755  ablsubsub23  19765  mulgdi  19767  mulgsubdi  19770  dprdss  19972  dprdf1o  19975  dprdsn  19979  dmdprdsplit  19990  pgpfac1lem5  20022  omndmul2  20074  prdsrngd  20123  imasrng  20124  srgdilem  20139  ringdilem  20196  ringrng  20232  prdsringd  20268  imasring  20278  opprrng  20293  mulgass3  20301  dvrass  20356  dvrdir  20360  subrgunit  20535  issubrg2  20537  isdomn4  20661  abvdiv  20774  lss1  20901  lsssn0  20911  islss3  20922  prdslmodd  20932  islmhm2  21002  lspsolv  21110  lbsextlem4  21128  sralmod  21151  rnglidl1  21199  ipdi  21607  ipsubdir  21609  ipsubdi  21610  ipassr  21613  ipassr2  21614  isphld  21621  ocvlss  21639  sraassab  21835  sraassaOLD  21837  psrlmod  21927  psrring  21937  psrassa  21940  mpllsslem  21967  mamudm  22351  matring  22399  matassa  22400  ofco2  22407  scmatlss  22481  ma1repveval  22527  mdetunilem1  22568  mdetunilem9  22576  monmatcollpw  22735  iinopn  22858  restopnb  23131  subbascn  23210  hausnei2  23309  nrmsep2  23312  isnrm3  23315  t1sep  23326  regsep2  23332  dnsconst  23334  dfconn2  23375  dislly  23453  tx1stc  23606  qtophmeo  23773  filss  23809  infil  23819  fsubbas  23823  filssufilg  23867  hauspwpwf1  23943  cnextcn  24023  tmdcn2  24045  psmettri  24267  isxmet2d  24283  xmettri  24307  xmetres2  24317  bldisj  24354  blss2ps  24359  blss2  24360  xmstri2  24422  mstri2  24423  xmstri  24424  mstri  24425  xmstri3  24426  mstri3  24427  msrtri  24428  comet  24469  met2ndci  24478  ngprcan  24566  ngplcan  24567  ngpsubcan  24570  nmtri2  24583  nrgdsdi  24621  nrgdsdir  24622  nlmdsdi  24637  nlmdsdir  24638  blcvx  24754  iocopnst  24905  icccvx  24916  pi1grplem  25017  pi1xfrf  25021  pi1cof  25027  clmpm1dir  25071  cmodscmulexp  25090  cvsdiv  25100  cvsdivcl  25101  cphdivcl  25150  cphsubdir  25176  cphsubdi  25177  bcthlem5  25296  rrxcph  25360  volfiniun  25516  volcn  25575  itg1val2  25653  dvconst  25886  dvlip  25966  ftc1a  26012  ulmdvlem3  26379  ang180  26792  cvxcl  26963  scvxcvx  26964  sgmmul  27180  logexprlim  27204  dchrabl  27233  nosupbnd1  27694  noinfbnd1lem5  27707  noinfbnd1  27709  sltssep  27775  addscom  27974  addbday  28026  addsdi  28163  mulsass  28174  motgrp  28627  iscgra1  28894  cgrane2  28897  cgrane4  28899  cgrahl1  28900  cgrahl2  28901  cgracgr  28902  cgratr  28907  cgrabtwn  28910  cgrahl  28911  dfcgra2  28914  sacgr  28915  f1otrge  28956  xmstrkgc  28970  colinearalglem1  28991  colinearalg  28995  axcgrtr  29000  axlowdimlem16  29042  axeuclidlem  29047  axcontlem4  29052  axcontlem7  29055  axcontlem12  29060  eengtrkg  29071  eengtrkge  29072  edglnl  29228  subgruhgredgd  29369  nbfusgrlevtxm2  29463  upgrwlkdvde  29822  crctcshwlkn0lem5  29899  crctcshwlkn0  29906  usgrwwlks2on  30043  umgrwwlks2on  30044  rusgrnumwwlks  30062  clwlkclwwlkfo  30096  3spthd  30263  frgr2wwlkeqm  30418  dlwwlknondlwlknonf1o  30452  numclwwlk5  30475  friendship  30486  grpomuldivass  30628  ablodivdiv4  30641  dipdi  30930  dipsubdi  30936  disjdsct  32792  archiabllem2c  33288  dvrcan5  33329  rloccring  33363  reofld  33435  eqgvscpbl  33442  qusvsval  33444  quslmod  33450  quslmhm  33451  prmidlc  33540  ssdifidl  33549  ssmxidl  33566  ply1degltlss  33688  r1plmhm  33702  drgextlsp  33770  ccfldsrarelvec  33848  constrconj  33922  constrfin  33923  constrelextdg2  33924  pstmfval  34073  qqhval2lem  34158  qqhvq  34164  esumcvg  34263  sigaclcu  34294  measdivcst  34401  measdivcstALTV  34402  carsggect  34495  tgoldbachgtd  34839  bnj970  35122  bnj910  35123  erdszelem9  35412  cvmseu  35489  elmrsubrn  35733  r1peuqusdeg1  35856  cgrid2  36216  btwncomim  36226  btwnswapid  36230  trisegint  36241  cgrxfr  36268  btwnxfr  36269  brofs2  36290  brifs2  36291  endofsegid  36298  btwnconn1lem11  36310  btwnconn2  36315  segcon2  36318  seglemin  36326  segletr  36327  btwnsegle  36330  colinbtwnle  36331  broutsideof2  36335  btwnoutside  36338  broutsideof3  36339  outsideoftr  36342  outsidele  36345  ellines  36365  linethrueu  36369  weiunpo  36678  unbdqndv2  36730  poimirlem28  37893  ftc1anc  37946  sdclem1  37988  sstotbnd2  38019  ismndo1  38118  zerdivemp1x  38192  isdrngo2  38203  iscringd  38243  lsmsat  39378  lfladdcl  39441  lflnegcl  39445  lflvscl  39447  lshpkrlem4  39483  lshpkrlem6  39485  ldualgrplem  39515  lduallmodlem  39522  latmassOLD  39599  latm12  39600  latm32  39601  latmrot  39602  latmmdiN  39604  latmmdir  39605  omlfh1N  39628  omlfh3N  39629  cvrnbtwn2  39645  cvlexchb1  39700  cvlexch3  39702  cvlexch4N  39703  cvlatexchb1  39704  cvlsupr2  39713  hlatjass  39740  hlatj12  39741  hlatj32  39742  cvrat  39792  atcvrj0  39798  cvrat2  39799  atltcvr  39805  atexchltN  39811  cvrat3  39812  cvrat4  39813  atbtwnexOLDN  39817  atbtwnex  39818  3dimlem3  39831  3dimlem3OLDN  39832  3at  39860  2atneat  39885  llncmp  39892  2at0mat0  39895  2atmat0  39896  islpln2a  39918  llncvrlpln  39928  lplncmp  39932  3atnelvolN  39956  4atlem11  39979  lplncvrlvol  39986  lvolcmp  39987  2atm2atN  40155  elpaddatriN  40173  elpadd2at2  40177  paddasslem8  40197  paddasslem17  40206  paddass  40208  padd12N  40209  paddssw1  40213  pmodlem2  40217  pmodN  40220  pmapjlln1  40225  atmod1i2  40229  pexmidlem2N  40341  pexmidlem7N  40346  pl42lem2N  40350  pl42lem3N  40351  pl42lem4N  40352  pl42N  40353  lhp2lt  40371  lhpm0atN  40399  lautlt  40461  lautcvr  40462  lautj  40463  lautm  40464  ltrneq2  40518  cdleme1b  40596  cdleme3b  40599  cdleme3c  40600  cdleme9b  40622  cdlemefs27cl  40783  cdleme42mN  40857  cdlemg4c  40982  trljco  41110  tgrpgrplem  41119  tendoplass  41153  tendodi1  41154  tendodi2  41155  erngplus2  41174  erngplus2-rN  41182  cdlemk36  41283  erngdvlem3  41360  erngdvlem3-rN  41368  dvaplusgv  41380  tendospass  41389  tendospdi1  41390  dvalveclem  41395  dialss  41416  dvhvaddass  41467  dvhopvsca  41472  dvhlveclem  41478  diblss  41540  diclss  41563  diclspsn  41564  cdlemn11pre  41580  dihmeetlem12N  41688  dihmeetlem16N  41692  dihmeetlem17N  41693  dvh4dimN  41817  lpolsatN  41858  lpolpolsatN  41859  dochpolN  41860  lclkr  41903  lclkrs  41909  lcfr  41955  lcmineqlem13  42405  aks6d1c1  42480  irrapxlem6  43178  jm2.26lem3  43352  mpaamn  43507  mendring  43539  mendlmod  43540  mendassa  43541  nnoeomeqom  43663  omabs2  43683  neicvgel1  44469  rfcnpre4  45388  fmuldfeq  45937  stoweidlem43  46395  stoweidlem52  46404  stoweidlem53  46405  stoweidlem56  46408  issmfgt  47108  issmfge  47122  iccelpart  47787  prproropf1olem1  47857  fmtnoprmfac1  47919  fmtnoprmfac2  47921  isubgr3stgrlem2  48321  isubgr3stgrlem4  48323  grlimgrtrilem1  48355  copissgrp  48522  cznrng  48615  funcringcsetcALTV2lem9  48652  funcringcsetclem9ALTV  48675  linccl  48768  lincsumscmcl  48787  ldepsprlem  48826  lincresunit3lem1  48833  itsclc0yqe  49115  resipos  49328  topdlat  49357  catprs  49364  endmndlem  49368  idmon  49373  idepi  49374  thincmon  49786  thincepi  49787  functhinclem1  49797  grptcmon  49946  grptcepi  49947