Theorem simpr3 1209

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 488	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜃)
2	1	3ad2antr3 1203	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simpr13  1272  simpr23  1275  simpr33  1278  simp1r3  1284  simp2r3  1290  simp3r3  1296  3anandis  1491  funopsn  7126  funopsnOLD  7127  fpr2g  7191  isopolem  7325  fr3nr  7751  sexp3  8128  suppfnss  8164  naddass  8662  dif1en  9126  elfir  9358  intrnfi  9359  fisupcl  9413  cnfcomlem  9651  ttrclss  9672  dmttrcl  9673  rnttrcl  9674  ttrclselem2  9678  ackbij1lem15  10186  pwfseqlem4a  10616  pwfseqlem4  10617  eluzuzle  12845  xlesubadd  13263  elioc2  13410  elico2  13411  elicc2  13412  fseq1p1m1  13600  ccatswrd  14679  pfxccat3a  14748  2cshw  14823  tanadd  16182  dvds2ln  16306  prmgaplem5  17074  prmgaplem8  17077  cshwsidrepsw  17112  ressress  17266  f1ovscpbl  17539  mreexexlem4d  17662  mreexexd  17663  2oppccomf  17740  fthmon  17945  fuccocl  17983  fucidcl  17984  invfuc  17993  initoeu2lem1  18030  curf2cl  18246  yonedalem4c  18292  yonedalem3  18295  pospo  18358  latjle12  18465  latjlej1  18468  latnlej2  18474  latlem12  18481  latmlem1  18484  latledi  18492  latjass  18498  latj12  18499  latj32  18500  latj13  18501  latj31  18502  latjrot  18503  latjjdi  18506  latjjdir  18507  latdisdlem  18511  prdssgrpd  18750  prdsmndd  18787  imasmnd2  18791  imasmnd  18792  frmdmnd  18876  grpsubadd  19053  grpaddsubass  19055  grpsubsub4  19058  grppnpcan2  19059  grpnpncan  19060  grpnnncan2  19062  imasgrp2  19080  imasgrp  19081  mulgnndir  19128  mulgnn0dir  19129  mulgnnass  19134  mulgnn0ass  19135  mulgass  19136  pwsmulg  19144  issubg2  19166  qusgrp  19210  kerf1ghm  19270  galcan  19327  gacan  19328  oppgmnd  19377  pmtrprfv  19476  pmtr3ncom  19498  psgnunilem3  19519  frgp0  19783  cmn32  19823  cmn12  19825  abladdsub  19835  ablsubaddsub  19837  ablsubsub23  19847  mulgdi  19849  mulgsubdi  19852  dprdss  20054  dprdf1o  20057  dprdsn  20061  dmdprdsplit  20072  pgpfac1lem5  20104  omndmul2  20156  prdsrngd  20205  imasrng  20206  srgdilem  20221  ringdilem  20278  ringrng  20314  prdsringd  20348  imasring  20358  opprrng  20373  mulgass3  20381  dvrass  20436  dvrdir  20440  subrgunit  20619  issubrg2  20621  isdomn4  20745  abvdiv  20858  lss1  20985  lsssn0  20995  islss3  21006  prdslmodd  21016  islmhm2  21085  lspsolv  21193  lbsextlem4  21211  sralmod  21234  rnglidl1  21282  ipdi  21672  ipsubdir  21674  ipsubdi  21675  ipassr  21678  ipassr2  21679  isphld  21686  ocvlss  21704  sraassab  21900  psrlmod  21991  psrring  22001  psrassa  22004  mpllsslem  22031  mamudm  22435  matring  22483  matassa  22484  ofco2  22491  scmatlss  22565  ma1repveval  22611  mdetunilem1  22652  mdetunilem9  22660  monmatcollpw  22819  iinopn  22942  restopnb  23215  subbascn  23294  hausnei2  23393  nrmsep2  23396  isnrm3  23399  t1sep  23410  regsep2  23416  dnsconst  23418  dfconn2  23459  dislly  23537  tx1stc  23690  qtophmeo  23857  filss  23893  infil  23903  fsubbas  23907  filssufilg  23951  hauspwpwf1  24027  cnextcn  24107  tmdcn2  24129  psmettri  24351  isxmet2d  24367  xmettri  24391  xmetres2  24401  bldisj  24438  blss2ps  24443  blss2  24444  xmstri2  24506  mstri2  24507  xmstri  24508  mstri  24509  xmstri3  24510  mstri3  24511  msrtri  24512  comet  24553  met2ndci  24562  ngprcan  24650  ngplcan  24651  ngpsubcan  24654  nmtri2  24667  nrgdsdi  24705  nrgdsdir  24706  nlmdsdi  24721  nlmdsdir  24722  blcvx  24838  iocopnst  24982  icccvx  24992  pi1grplem  25091  pi1xfrf  25095  pi1cof  25101  clmpm1dir  25145  cmodscmulexp  25164  cvsdiv  25174  cvsdivcl  25175  cphdivcl  25224  cphsubdir  25250  cphsubdi  25251  bcthlem5  25370  rrxcph  25434  volfiniun  25589  volcn  25648  itg1val2  25726  dvconst  25959  dvlip  26035  ftc1a  26079  ulmdvlem3  26442  ang180  26856  cvxcl  27026  scvxcvx  27027  sgmmul  27242  logexprlim  27266  dchrabl  27295  nosupbnd1  27755  noinfbnd1lem5  27768  noinfbnd1  27770  sltssep  27837  addscom  28036  addbday  28088  addsdi  28225  mulsass  28236  motgrp  28689  iscgra1  28956  cgrane2  28959  cgrane4  28961  cgrahl1  28962  cgrahl2  28963  cgracgr  28964  cgratr  28969  cgrabtwn  28972  cgrahl  28973  dfcgra2  28976  sacgr  28977  f1otrge  29018  xmstrkgc  29032  colinearalglem1  29053  colinearalg  29057  axcgrtr  29062  axlowdimlem16  29104  axeuclidlem  29109  axcontlem4  29114  axcontlem7  29117  axcontlem12  29122  eengtrkg  29133  eengtrkge  29134  edglnl  29290  subgruhgredgd  29431  nbfusgrlevtxm2  29525  upgrwlkdvde  29883  crctcshwlkn0lem5  29960  crctcshwlkn0  29967  usgrwwlks2on  30104  umgrwwlks2on  30105  rusgrnumwwlks  30123  clwlkclwwlkfo  30157  3spthd  30324  frgr2wwlkeqm  30479  dlwwlknondlwlknonf1o  30513  numclwwlk5  30536  friendship  30547  grpomuldivass  30690  ablodivdiv4  30703  dipdi  30992  dipsubdi  30998  disjdsct  32855  archiabllem2c  33336  dvrcan5  33377  rloccring  33413  reofld  33490  eqgvscpbl  33497  qusvsval  33499  quslmod  33505  quslmhm  33506  prmidlc  33595  ssdifidl  33605  ssmxidl  33623  ply1degltlss  33753  r1plmhm  33767  drgextlsp  33852  ccfldsrarelvec  33929  constrconj  34003  constrfin  34004  constrelextdg2  34005  pstmfval  34154  qqhval2lem  34239  qqhvq  34245  esumcvg  34344  sigaclcu  34375  measdivcst  34482  measdivcstALTV  34483  carsggect  34576  tgoldbachgtd  34920  bnj970  35206  bnj910  35207  erdszelem9  35513  cvmseu  35590  elmrsubrn  35834  r1peuqusdeg1  35957  cgrid2  36317  btwncomim  36327  btwnswapid  36331  trisegint  36342  cgrxfr  36369  btwnxfr  36370  brofs2  36391  brifs2  36392  endofsegid  36399  btwnconn1lem11  36411  btwnconn2  36416  segcon2  36419  seglemin  36427  segletr  36428  btwnsegle  36431  colinbtwnle  36432  broutsideof2  36436  btwnoutside  36439  broutsideof3  36440  outsideoftr  36443  outsidele  36446  ellines  36466  linethrueu  36470  nmulprop  36504  weiunpo  36789  unbdqndv2  36913  poimirlem28  38111  ftc1anc  38164  sdclem1  38206  sstotbnd2  38237  ismndo1  38336  zerdivemp1x  38410  isdrngo2  38421  iscringd  38461  lsmsat  39596  lfladdcl  39659  lflnegcl  39663  lflvscl  39665  lshpkrlem4  39701  lshpkrlem6  39703  ldualgrplem  39733  lduallmodlem  39740  latmassOLD  39817  latm12  39818  latm32  39819  latmrot  39820  latmmdiN  39822  latmmdir  39823  omlfh1N  39846  omlfh3N  39847  cvrnbtwn2  39863  cvlexchb1  39918  cvlexch3  39920  cvlexch4N  39921  cvlatexchb1  39922  cvlsupr2  39931  hlatjass  39958  hlatj12  39959  hlatj32  39960  cvrat  40010  atcvrj0  40016  cvrat2  40017  atltcvr  40023  atexchltN  40029  cvrat3  40030  cvrat4  40031  atbtwnexOLDN  40035  atbtwnex  40036  3dimlem3  40049  3dimlem3OLDN  40050  3at  40078  2atneat  40103  llncmp  40110  2at0mat0  40113  2atmat0  40114  islpln2a  40136  llncvrlpln  40146  lplncmp  40150  3atnelvolN  40174  4atlem11  40197  lplncvrlvol  40204  lvolcmp  40205  2atm2atN  40373  elpaddatriN  40391  elpadd2at2  40395  paddasslem8  40415  paddasslem17  40424  paddass  40426  padd12N  40427  paddssw1  40431  pmodlem2  40435  pmodN  40438  pmapjlln1  40443  atmod1i2  40447  pexmidlem2N  40559  pexmidlem7N  40564  pl42lem2N  40568  pl42lem3N  40569  pl42lem4N  40570  pl42N  40571  lhp2lt  40589  lhpm0atN  40617  lautlt  40679  lautcvr  40680  lautj  40681  lautm  40682  ltrneq2  40736  cdleme1b  40814  cdleme3b  40817  cdleme3c  40818  cdleme9b  40840  cdlemefs27cl  41001  cdleme42mN  41075  cdlemg4c  41200  trljco  41328  tgrpgrplem  41337  tendoplass  41371  tendodi1  41372  tendodi2  41373  erngplus2  41392  erngplus2-rN  41400  cdlemk36  41501  erngdvlem3  41578  erngdvlem3-rN  41586  dvaplusgv  41598  tendospass  41607  tendospdi1  41608  dvalveclem  41613  dialss  41634  dvhvaddass  41685  dvhopvsca  41690  dvhlveclem  41696  diblss  41758  diclss  41781  diclspsn  41782  cdlemn11pre  41798  dihmeetlem12N  41906  dihmeetlem16N  41910  dihmeetlem17N  41911  dvh4dimN  42035  lpolsatN  42076  lpolpolsatN  42077  dochpolN  42078  lclkr  42121  lclkrs  42127  lcfr  42173  lcmineqlem13  42622  aks6d1c1  42697  irrapxlem6  43368  jm2.26lem3  43542  mpaamn  43697  mendring  43729  mendlmod  43730  mendassa  43731  nnoeomeqom  43853  omabs2  43873  neicvgel1  44659  rfcnpre4  45578  fmuldfeq  46123  stoweidlem43  46581  stoweidlem52  46590  stoweidlem53  46591  stoweidlem56  46594  issmfgt  47294  issmfge  47308  iccelpart  48003  prproropf1olem1  48073  fmtnoprmfac1  48138  fmtnoprmfac2  48140  isubgr3stgrlem2  48553  isubgr3stgrlem4  48555  grlimgrtrilem1  48587  copissgrp  48754  cznrng  48847  funcringcsetcALTV2lem9  48884  funcringcsetclem9ALTV  48907  linccl  49000  lincsumscmcl  49019  ldepsprlem  49058  lincresunit3lem1  49065  itsclc0yqe  49347  resipos  49560  topdlat  49589  catprs  49596  endmndlem  49600  idmon  49605  idepi  49606  thincmon  50018  thincepi  50019  functhinclem1  50029  grptcmon  50178  grptcepi  50179