Theorem simpr3 1215

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

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

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 1105

This theorem is referenced by:  simpr13  1278  simpr23  1281  simpr33  1284  simp1r3  1290  simp2r3  1296  simp3r3  1302  3anandis  1500  funopsn  7146  funopsnOLD  7147  fpr2g  7211  isopolem  7345  fr3nr  7772  sexp3  8150  suppfnss  8186  naddass  8684  dif1en  9147  elfir  9376  intrnfi  9377  fisupcl  9431  cnfcomlem  9669  ttrclss  9690  dmttrcl  9691  rnttrcl  9692  ttrclselem2  9696  ackbij1lem15  10217  pwfseqlem4a  10647  pwfseqlem4  10648  eluzuzle  12872  xlesubadd  13290  elioc2  13437  elico2  13438  elicc2  13439  fseq1p1m1  13628  ccatswrd  14708  pfxccat3a  14777  2cshw  14852  tanadd  16224  dvds2ln  16348  prmgaplem5  17116  prmgaplem8  17119  cshwsidrepsw  17154  ressress  17308  f1ovscpbl  17581  mreexexlem4d  17704  mreexexd  17705  2oppccomf  17782  fthmon  17987  fuccocl  18025  fucidcl  18026  invfuc  18035  initoeu2lem1  18072  curf2cl  18288  yonedalem4c  18334  yonedalem3  18337  pospo  18400  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  18792  prdsmndd  18829  imasmnd2  18833  imasmnd  18834  frmdmnd  18919  grpsubadd  19095  grpaddsubass  19097  grpsubsub4  19100  grppnpcan2  19101  grpnpncan  19102  grpnnncan2  19104  imasgrp2  19122  imasgrp  19123  mulgnndir  19170  mulgnn0dir  19171  mulgnnass  19176  mulgnn0ass  19177  mulgass  19178  pwsmulg  19186  issubg2  19209  qusgrp  19258  kerf1ghm  19318  galcan  19375  gacan  19376  oppgmnd  19425  pmtrprfv  19524  pmtr3ncom  19546  psgnunilem3  19567  frgp0  19831  cmn32  19871  cmn12  19873  abladdsub  19883  ablsubaddsub  19885  ablsubsub23  19895  mulgdi  19897  mulgsubdi  19900  dprdss  20102  dprdf1o  20105  dprdsn  20109  dmdprdsplit  20120  pgpfac1lem5  20152  omndmul2  20204  prdsrngd  20255  imasrng  20256  srgdilem  20275  ringdilem  20332  ringrng  20369  prdsringd  20403  imasring  20413  opprrng  20428  mulgass3  20436  dvrass  20491  dvrdir  20495  subrgunit  20676  issubrg2  20678  isdomn4  20801  abvdiv  20913  lss1  21040  lsssn0  21050  islss3  21061  prdslmodd  21071  islmhm2  21140  lspsolv  21248  lbsextlem4  21266  sralmod  21289  rnglidl1  21339  prmidlc  21454  ssdifidl  21466  ipdi  21771  ipsubdir  21773  ipsubdi  21774  ipassr  21777  ipassr2  21778  isphld  21785  ocvlss  21803  sraassab  21999  psrlmod  22090  psrring  22100  psrassa  22103  mpllsslem  22130  mamudm  22533  matring  22581  matassa  22582  ofco2  22589  scmatlss  22663  ma1repveval  22709  mdetunilem1  22750  mdetunilem9  22758  monmatcollpw  22917  iinopn  23040  restopnb  23313  subbascn  23392  hausnei2  23491  nrmsep2  23494  isnrm3  23497  t1sep  23508  regsep2  23514  dnsconst  23516  dfconn2  23557  dislly  23635  tx1stc  23788  qtophmeo  23955  filss  23991  infil  24001  fsubbas  24005  filssufilg  24049  hauspwpwf1  24125  cnextcn  24205  tmdcn2  24227  psmettri  24449  isxmet2d  24465  xmettri  24489  xmetres2  24499  bldisj  24536  blss2ps  24541  blss2  24542  xmstri2  24604  mstri2  24605  xmstri  24606  mstri  24607  xmstri3  24608  mstri3  24609  msrtri  24610  comet  24651  met2ndci  24660  ngprcan  24748  ngplcan  24749  ngpsubcan  24752  nmtri2  24765  nrgdsdi  24803  nrgdsdir  24804  nlmdsdi  24819  nlmdsdir  24820  blcvx  24936  iocopnst  25080  icccvx  25090  pi1grplem  25189  pi1xfrf  25193  pi1cof  25199  clmpm1dir  25243  cmodscmulexp  25262  cvsdiv  25272  cvsdivcl  25273  cphdivcl  25322  cphsubdir  25348  cphsubdi  25349  bcthlem5  25468  rrxcph  25532  volfiniun  25687  volcn  25746  itg1val2  25824  dvconst  26057  dvlip  26133  ftc1a  26177  ulmdvlem3  26543  ang180  26957  cvxcl  27127  scvxcvx  27128  sgmmul  27343  logexprlim  27367  dchrabl  27396  nosupbnd1  27856  noinfbnd1lem5  27869  noinfbnd1  27871  sltssep  27938  addscom  28137  addbday  28189  addsdi  28326  mulsass  28337  motgrp  28790  iscgra1  29099  cgrane2  29102  cgrane4  29104  cgrahl1  29105  cgrahl2  29106  cgracgr  29107  cgratr  29112  cgrabtwn  29115  cgrahl  29116  dfcgra2  29119  sacgr  29120  f1otrge  29199  xmstrkgc  29213  colinearalglem1  29234  colinearalg  29238  axcgrtr  29243  axlowdimlem16  29285  axeuclidlem  29290  axcontlem4  29295  axcontlem7  29298  axcontlem12  29303  eengtrkg  29314  eengtrkge  29315  edglnl  29471  subgruhgredgd  29612  nbfusgrlevtxm2  29706  upgrwlkdvde  30064  crctcshwlkn0lem5  30141  crctcshwlkn0  30148  usgrwwlks2on  30285  umgrwwlks2on  30286  rusgrnumwwlks  30304  clwlkclwwlkfo  30338  3spthd  30505  frgr2wwlkeqm  30660  dlwwlknondlwlknonf1o  30694  numclwwlk5  30717  friendship  30728  grpomuldivass  30871  ablodivdiv4  30884  dipdi  31173  dipsubdi  31179  disjdsct  33026  archiabllem2c  33493  dvrcan5  33533  rloccring  33569  reofld  33641  eqgvscpbl  33648  qusvsval  33650  quslmod  33656  quslmhm  33657  ssmxidl  33735  ply1degltlss  33864  r1plmhm  33877  drgextlsp  33962  ccfldsrarelvec  34039  constrconj  34113  constrfin  34114  constrelextdg2  34115  pstmfval  34264  qqhval2lem  34349  qqhvq  34355  esumcvg  34454  sigaclcu  34485  measdivcst  34592  measdivcstALTV  34593  carsggect  34686  tgoldbachgtd  35027  bnj970  35313  bnj910  35314  erdszelem9  35669  cvmseu  35746  elmrsubrn  35990  r1peuqusdeg1  36113  cgrid2  36473  btwncomim  36483  btwnswapid  36487  trisegint  36498  cgrxfr  36525  btwnxfr  36526  brofs2  36547  brifs2  36548  endofsegid  36555  btwnconn1lem11  36567  btwnconn2  36572  segcon2  36575  seglemin  36583  segletr  36584  btwnsegle  36587  colinbtwnle  36588  broutsideof2  36592  btwnoutside  36595  broutsideof3  36596  outsideoftr  36599  outsidele  36602  ellines  36622  linethrueu  36626  nmulprop  36660  weiunpo  36954  unbdqndv2  37078  poimirlem28  38277  ftc1anc  38330  sdclem1  38372  sstotbnd2  38403  ismndo1  38502  zerdivemp1x  38576  isdrngo2  38587  iscringd  38627  lsmsat  39760  lfladdcl  39823  lflnegcl  39827  lflvscl  39829  lshpkrlem4  39865  lshpkrlem6  39867  ldualgrplem  39897  lduallmodlem  39904  latmassOLD  39981  latm12  39982  latm32  39983  latmrot  39984  latmmdiN  39986  latmmdir  39987  omlfh1N  40010  omlfh3N  40011  cvrnbtwn2  40027  cvlexchb1  40082  cvlexch3  40084  cvlexch4N  40085  cvlatexchb1  40086  cvlsupr2  40095  hlatjass  40122  hlatj12  40123  hlatj32  40124  cvrat  40174  atcvrj0  40180  cvrat2  40181  atltcvr  40187  atexchltN  40193  cvrat3  40194  cvrat4  40195  atbtwnexOLDN  40199  atbtwnex  40200  3dimlem3  40213  3dimlem3OLDN  40214  3at  40242  2atneat  40267  llncmp  40274  2at0mat0  40277  2atmat0  40278  islpln2a  40300  llncvrlpln  40310  lplncmp  40314  3atnelvolN  40338  4atlem11  40361  lplncvrlvol  40368  lvolcmp  40369  2atm2atN  40537  elpaddatriN  40555  elpadd2at2  40559  paddasslem8  40579  paddasslem17  40588  paddass  40590  padd12N  40591  paddssw1  40595  pmodlem2  40599  pmodN  40602  pmapjlln1  40607  atmod1i2  40611  pexmidlem2N  40723  pexmidlem7N  40728  pl42lem2N  40732  pl42lem3N  40733  pl42lem4N  40734  pl42N  40735  lhp2lt  40753  lhpm0atN  40781  lautlt  40843  lautcvr  40844  lautj  40845  lautm  40846  ltrneq2  40900  cdleme1b  40978  cdleme3b  40981  cdleme3c  40982  cdleme9b  41004  cdlemefs27cl  41165  cdleme42mN  41239  cdlemg4c  41364  trljco  41492  tgrpgrplem  41501  tendoplass  41535  tendodi1  41536  tendodi2  41537  erngplus2  41556  erngplus2-rN  41564  cdlemk36  41665  erngdvlem3  41742  erngdvlem3-rN  41750  dvaplusgv  41762  tendospass  41771  tendospdi1  41772  dvalveclem  41777  dialss  41798  dvhvaddass  41849  dvhopvsca  41854  dvhlveclem  41860  diblss  41922  diclss  41945  diclspsn  41946  cdlemn11pre  41962  dihmeetlem12N  42070  dihmeetlem16N  42074  dihmeetlem17N  42075  dvh4dimN  42199  lpolsatN  42240  lpolpolsatN  42241  dochpolN  42242  lclkr  42285  lclkrs  42291  lcfr  42337  lcmineqlem13  42786  aks6d1c1  42861  irrapxlem6  43534  jm2.26lem3  43708  mpaamn  43863  mendring  43895  mendlmod  43896  mendassa  43897  nnoeomeqom  44019  omabs2  44039  neicvgel1  44825  rfcnpre4  45734  fmuldfeq  46279  stoweidlem43  46737  stoweidlem52  46746  stoweidlem53  46747  stoweidlem56  46750  issmfgt  47450  issmfge  47464  iccelpart  48159  prproropf1olem1  48229  fmtnoprmfac1  48294  fmtnoprmfac2  48296  isubgr3stgrlem2  48709  isubgr3stgrlem4  48711  grlimgrtrilem1  48743  copissgrp  48910  cznrng  49003  funcringcsetcALTV2lem9  49040  funcringcsetclem9ALTV  49063  idomcanl  49089  linccl  49171  lincsumscmcl  49190  ldepsprlem  49229  lincresunit3lem1  49236  itsclc0yqe  49518  resipos  49730  topdlat  49759  catprs  49766  endmndlem  49770  idmon  49775  idepi  49776  thincmon  50188  thincepi  50189  functhinclem1  50199  grptcmon  50348  grptcepi  50349