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  7101  funopsnOLD  7102  fpr2g  7166  isopolem  7300  fr3nr  7726  sexp3  8103  suppfnss  8139  naddass  8632  dif1en  9096  elfir  9328  intrnfi  9329  fisupcl  9383  cnfcomlem  9620  ttrclss  9641  dmttrcl  9642  rnttrcl  9643  ttrclselem2  9647  ackbij1lem15  10155  pwfseqlem4a  10584  pwfseqlem4  10585  eluzuzle  12797  xlesubadd  13215  elioc2  13362  elico2  13363  elicc2  13364  fseq1p1m1  13552  ccatswrd  14631  pfxccat3a  14700  2cshw  14775  tanadd  16134  dvds2ln  16258  prmgaplem5  17026  prmgaplem8  17029  cshwsidrepsw  17064  ressress  17217  f1ovscpbl  17490  mreexexlem4d  17613  mreexexd  17614  2oppccomf  17691  fthmon  17896  fuccocl  17934  fucidcl  17935  invfuc  17944  initoeu2lem1  17981  curf2cl  18197  yonedalem4c  18243  yonedalem3  18246  pospo  18309  latjle12  18416  latjlej1  18419  latnlej2  18425  latlem12  18432  latmlem1  18435  latledi  18443  latjass  18449  latj12  18450  latj32  18451  latj13  18452  latj31  18453  latjrot  18454  latjjdi  18457  latjjdir  18458  latdisdlem  18462  prdssgrpd  18701  prdsmndd  18738  imasmnd2  18742  imasmnd  18743  frmdmnd  18827  grpsubadd  19004  grpaddsubass  19006  grpsubsub4  19009  grppnpcan2  19010  grpnpncan  19011  grpnnncan2  19013  imasgrp2  19031  imasgrp  19032  mulgnndir  19079  mulgnn0dir  19080  mulgnnass  19085  mulgnn0ass  19086  mulgass  19087  pwsmulg  19095  issubg2  19117  qusgrp  19161  kerf1ghm  19222  galcan  19279  gacan  19280  oppgmnd  19329  pmtrprfv  19428  pmtr3ncom  19450  psgnunilem3  19471  frgp0  19735  cmn32  19775  cmn12  19777  abladdsub  19787  ablsubaddsub  19789  ablsubsub23  19799  mulgdi  19801  mulgsubdi  19804  dprdss  20006  dprdf1o  20009  dprdsn  20013  dmdprdsplit  20024  pgpfac1lem5  20056  omndmul2  20108  prdsrngd  20157  imasrng  20158  srgdilem  20173  ringdilem  20230  ringrng  20266  prdsringd  20300  imasring  20310  opprrng  20325  mulgass3  20333  dvrass  20388  dvrdir  20392  subrgunit  20567  issubrg2  20569  isdomn4  20693  abvdiv  20806  lss1  20933  lsssn0  20943  islss3  20954  prdslmodd  20964  islmhm2  21033  lspsolv  21141  lbsextlem4  21159  sralmod  21182  rnglidl1  21230  ipdi  21620  ipsubdir  21622  ipsubdi  21623  ipassr  21626  ipassr2  21627  isphld  21634  ocvlss  21652  sraassab  21848  psrlmod  21938  psrring  21948  psrassa  21951  mpllsslem  21978  mamudm  22360  matring  22408  matassa  22409  ofco2  22416  scmatlss  22490  ma1repveval  22536  mdetunilem1  22577  mdetunilem9  22585  monmatcollpw  22744  iinopn  22867  restopnb  23140  subbascn  23219  hausnei2  23318  nrmsep2  23321  isnrm3  23324  t1sep  23335  regsep2  23341  dnsconst  23343  dfconn2  23384  dislly  23462  tx1stc  23615  qtophmeo  23782  filss  23818  infil  23828  fsubbas  23832  filssufilg  23876  hauspwpwf1  23952  cnextcn  24032  tmdcn2  24054  psmettri  24276  isxmet2d  24292  xmettri  24316  xmetres2  24326  bldisj  24363  blss2ps  24368  blss2  24369  xmstri2  24431  mstri2  24432  xmstri  24433  mstri  24434  xmstri3  24435  mstri3  24436  msrtri  24437  comet  24478  met2ndci  24487  ngprcan  24575  ngplcan  24576  ngpsubcan  24579  nmtri2  24592  nrgdsdi  24630  nrgdsdir  24631  nlmdsdi  24646  nlmdsdir  24647  blcvx  24763  iocopnst  24907  icccvx  24917  pi1grplem  25016  pi1xfrf  25020  pi1cof  25026  clmpm1dir  25070  cmodscmulexp  25089  cvsdiv  25099  cvsdivcl  25100  cphdivcl  25149  cphsubdir  25175  cphsubdi  25176  bcthlem5  25295  rrxcph  25359  volfiniun  25514  volcn  25573  itg1val2  25651  dvconst  25884  dvlip  25960  ftc1a  26004  ulmdvlem3  26367  ang180  26778  cvxcl  26948  scvxcvx  26949  sgmmul  27164  logexprlim  27188  dchrabl  27217  nosupbnd1  27678  noinfbnd1lem5  27691  noinfbnd1  27693  sltssep  27759  addscom  27958  addbday  28010  addsdi  28147  mulsass  28158  motgrp  28611  iscgra1  28878  cgrane2  28881  cgrane4  28883  cgrahl1  28884  cgrahl2  28885  cgracgr  28886  cgratr  28891  cgrabtwn  28894  cgrahl  28895  dfcgra2  28898  sacgr  28899  f1otrge  28940  xmstrkgc  28954  colinearalglem1  28975  colinearalg  28979  axcgrtr  28984  axlowdimlem16  29026  axeuclidlem  29031  axcontlem4  29036  axcontlem7  29039  axcontlem12  29044  eengtrkg  29055  eengtrkge  29056  edglnl  29212  subgruhgredgd  29353  nbfusgrlevtxm2  29447  upgrwlkdvde  29805  crctcshwlkn0lem5  29882  crctcshwlkn0  29889  usgrwwlks2on  30026  umgrwwlks2on  30027  rusgrnumwwlks  30045  clwlkclwwlkfo  30079  3spthd  30246  frgr2wwlkeqm  30401  dlwwlknondlwlknonf1o  30435  numclwwlk5  30458  friendship  30469  grpomuldivass  30612  ablodivdiv4  30625  dipdi  30914  dipsubdi  30920  disjdsct  32776  archiabllem2c  33256  dvrcan5  33297  rloccring  33331  reofld  33403  eqgvscpbl  33410  qusvsval  33412  quslmod  33418  quslmhm  33419  prmidlc  33508  ssdifidl  33517  ssmxidl  33534  ply1degltlss  33656  r1plmhm  33670  drgextlsp  33738  ccfldsrarelvec  33815  constrconj  33889  constrfin  33890  constrelextdg2  33891  pstmfval  34040  qqhval2lem  34125  qqhvq  34131  esumcvg  34230  sigaclcu  34261  measdivcst  34368  measdivcstALTV  34369  carsggect  34462  tgoldbachgtd  34806  bnj970  35089  bnj910  35090  erdszelem9  35381  cvmseu  35458  elmrsubrn  35702  r1peuqusdeg1  35825  cgrid2  36185  btwncomim  36195  btwnswapid  36199  trisegint  36210  cgrxfr  36237  btwnxfr  36238  brofs2  36259  brifs2  36260  endofsegid  36267  btwnconn1lem11  36279  btwnconn2  36284  segcon2  36287  seglemin  36295  segletr  36296  btwnsegle  36299  colinbtwnle  36300  broutsideof2  36304  btwnoutside  36307  broutsideof3  36308  outsideoftr  36311  outsidele  36314  ellines  36334  linethrueu  36338  weiunpo  36647  unbdqndv2  36771  poimirlem28  37969  ftc1anc  38022  sdclem1  38064  sstotbnd2  38095  ismndo1  38194  zerdivemp1x  38268  isdrngo2  38279  iscringd  38319  lsmsat  39454  lfladdcl  39517  lflnegcl  39521  lflvscl  39523  lshpkrlem4  39559  lshpkrlem6  39561  ldualgrplem  39591  lduallmodlem  39598  latmassOLD  39675  latm12  39676  latm32  39677  latmrot  39678  latmmdiN  39680  latmmdir  39681  omlfh1N  39704  omlfh3N  39705  cvrnbtwn2  39721  cvlexchb1  39776  cvlexch3  39778  cvlexch4N  39779  cvlatexchb1  39780  cvlsupr2  39789  hlatjass  39816  hlatj12  39817  hlatj32  39818  cvrat  39868  atcvrj0  39874  cvrat2  39875  atltcvr  39881  atexchltN  39887  cvrat3  39888  cvrat4  39889  atbtwnexOLDN  39893  atbtwnex  39894  3dimlem3  39907  3dimlem3OLDN  39908  3at  39936  2atneat  39961  llncmp  39968  2at0mat0  39971  2atmat0  39972  islpln2a  39994  llncvrlpln  40004  lplncmp  40008  3atnelvolN  40032  4atlem11  40055  lplncvrlvol  40062  lvolcmp  40063  2atm2atN  40231  elpaddatriN  40249  elpadd2at2  40253  paddasslem8  40273  paddasslem17  40282  paddass  40284  padd12N  40285  paddssw1  40289  pmodlem2  40293  pmodN  40296  pmapjlln1  40301  atmod1i2  40305  pexmidlem2N  40417  pexmidlem7N  40422  pl42lem2N  40426  pl42lem3N  40427  pl42lem4N  40428  pl42N  40429  lhp2lt  40447  lhpm0atN  40475  lautlt  40537  lautcvr  40538  lautj  40539  lautm  40540  ltrneq2  40594  cdleme1b  40672  cdleme3b  40675  cdleme3c  40676  cdleme9b  40698  cdlemefs27cl  40859  cdleme42mN  40933  cdlemg4c  41058  trljco  41186  tgrpgrplem  41195  tendoplass  41229  tendodi1  41230  tendodi2  41231  erngplus2  41250  erngplus2-rN  41258  cdlemk36  41359  erngdvlem3  41436  erngdvlem3-rN  41444  dvaplusgv  41456  tendospass  41465  tendospdi1  41466  dvalveclem  41471  dialss  41492  dvhvaddass  41543  dvhopvsca  41548  dvhlveclem  41554  diblss  41616  diclss  41639  diclspsn  41640  cdlemn11pre  41656  dihmeetlem12N  41764  dihmeetlem16N  41768  dihmeetlem17N  41769  dvh4dimN  41893  lpolsatN  41934  lpolpolsatN  41935  dochpolN  41936  lclkr  41979  lclkrs  41985  lcfr  42031  lcmineqlem13  42480  aks6d1c1  42555  irrapxlem6  43255  jm2.26lem3  43429  mpaamn  43584  mendring  43616  mendlmod  43617  mendassa  43618  nnoeomeqom  43740  omabs2  43760  neicvgel1  44546  rfcnpre4  45465  fmuldfeq  46013  stoweidlem43  46471  stoweidlem52  46480  stoweidlem53  46481  stoweidlem56  46484  issmfgt  47184  issmfge  47198  iccelpart  47893  prproropf1olem1  47963  fmtnoprmfac1  48028  fmtnoprmfac2  48030  isubgr3stgrlem2  48443  isubgr3stgrlem4  48445  grlimgrtrilem1  48477  copissgrp  48644  cznrng  48737  funcringcsetcALTV2lem9  48774  funcringcsetclem9ALTV  48797  linccl  48890  lincsumscmcl  48909  ldepsprlem  48948  lincresunit3lem1  48955  itsclc0yqe  49237  resipos  49450  topdlat  49479  catprs  49486  endmndlem  49490  idmon  49495  idepi  49496  thincmon  49908  thincepi  49909  functhinclem1  49919  grptcmon  50068  grptcepi  50069