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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr13  1278  simpr23  1281  simpr33  1284  simp1r3  1290  simp2r3  1296  simp3r3  1302  3anandis  1500  funopsn  7143  funopsnOLD  7144  fpr2g  7209  isopolem  7345  fr3nr  7775  sexp3  8154  suppfnss  8190  naddass  8690  dif1en  9161  elfir  9391  intrnfi  9392  fisupcl  9446  cnfcomlem  9684  ttrclss  9705  dmttrcl  9706  rnttrcl  9707  ttrclselem2  9711  ackbij1lem15  10292  pwfseqlem4a  10727  pwfseqlem4  10728  eluzuzle  12955  xlesubadd  13374  elioc2  13521  elico2  13522  elicc2  13523  fseq1p1m1  13712  ccatswrd  14798  pfxccat3a  14867  2cshw  14944  tanadd  16315  dvds2ln  16439  prmgaplem5  17213  prmgaplem8  17216  cshwsidrepsw  17251  ressress  17405  f1ovscpbl  17678  mreexexlem4d  17801  mreexexd  17802  2oppccomf  17879  fthmon  18084  fuccocl  18122  fucidcl  18123  invfuc  18132  initoeu2lem1  18169  curf2cl  18385  yonedalem4c  18431  yonedalem3  18434  pospo  18497  latjle12  18604  latjlej1  18607  latnlej2  18613  latlem12  18620  latmlem1  18623  latledi  18631  latjass  18637  latj12  18638  latj32  18639  latj13  18640  latj31  18641  latjrot  18642  latjjdi  18645  latjjdir  18646  latdisdlem  18650  prdssgrpd  18902  prdsmndd  18944  imasmnd2  18948  imasmnd  18949  frmdmnd  19035  grpsubadd  19218  grpaddsubass  19220  grpsubsub4  19223  grppnpcan2  19224  grpnpncan  19225  grpnnncan2  19227  imasgrp2  19245  imasgrp  19246  mulgnndir  19293  mulgnn0dir  19294  mulgnnass  19299  mulgnn0ass  19300  mulgass  19301  pwsmulg  19309  issubg2  19332  qusgrp  19381  kerf1ghm  19441  galcan  19498  gacan  19499  oppgmnd  19548  pmtrprfv  19647  pmtr3ncom  19669  psgnunilem3  19690  frgp0  19954  cmn32  19994  cmn12  19996  abladdsub  20006  ablsubaddsub  20008  ablsubsub23  20018  mulgdi  20020  mulgsubdi  20023  dprdss  20225  dprdf1o  20228  dprdsn  20232  dmdprdsplit  20243  pgpfac1lem5  20275  omndmul2  20327  prdsrngd  20378  imasrng  20379  srgdilem  20398  ringdilem  20456  ringrng  20494  prdsringd  20530  imasring  20540  opprrng  20555  mulgass3  20563  dvrass  20618  dvrdir  20622  subrgunit  20822  issubrg2  20824  isdomn4  20947  abvdiv  21066  lss1  21193  lsssn0  21203  islss3  21214  prdslmodd  21224  islmhm2  21293  lspsolv  21401  lbsextlem4  21419  sralmod  21442  rnglidl1  21492  prmidlc  21609  ssdifidl  21621  ipdi  21926  ipsubdir  21928  ipsubdi  21929  ipassr  21932  ipassr2  21933  isphld  21940  ocvlss  21958  sraassab  22156  psrlmod  22247  psrring  22257  psrassa  22260  mpllsslem  22287  mamudm  22690  matring  22738  matassa  22739  ofco2  22746  scmatlss  22820  ma1repveval  22866  mdetunilem1  22907  mdetunilem9  22915  monmatcollpw  23077  iinopn  23200  restopnb  23473  subbascn  23552  hausnei2  23651  nrmsep2  23654  isnrm3  23657  t1sep  23668  regsep2  23674  dnsconst  23676  dfconn2  23717  dislly  23796  tx1stc  23949  qtophmeo  24116  filss  24152  infil  24162  fsubbas  24166  filssufilg  24210  hauspwpwf1  24286  cnextcn  24366  tmdcn2  24388  psmettri  24610  isxmet2d  24626  xmettri  24650  xmetres2  24660  bldisj  24697  blss2ps  24702  blss2  24703  xmstri2  24765  mstri2  24766  xmstri  24767  mstri  24768  xmstri3  24769  mstri3  24770  msrtri  24771  comet  24812  met2ndci  24821  ngprcan  24909  ngplcan  24910  ngpsubcan  24913  nmtri2  24926  nrgdsdi  24964  nrgdsdir  24965  nlmdsdi  24980  nlmdsdir  24981  blcvx  25097  iocopnst  25241  icccvx  25251  pi1grplem  25350  pi1xfrf  25354  pi1cof  25360  clmpm1dir  25404  cmodscmulexp  25423  cvsdiv  25433  cvsdivcl  25434  cphdivcl  25483  cphsubdir  25509  cphsubdi  25510  bcthlem5  25629  rrxcph  25693  volfiniun  25848  volcn  25907  itg1val2  25985  dvconst  26217  dvlip  26293  ftc1a  26337  ulmdvlem3  26711  ang180  27124  cvxcl  27294  scvxcvx  27295  sgmmul  27510  logexprlim  27534  dchrabl  27563  nosupbnd1  28053  noinfbnd1lem5  28066  noinfbnd1  28068  sltssep  28135  addscom  28334  addbday  28386  addsdi  28523  mulsass  28534  motgrp  28988  iscgra1  29299  cgrane2  29302  cgrane4  29304  cgrahl1  29305  cgrahl2  29306  cgracgr  29307  cgratr  29312  cgrabtwn  29316  cgrahl  29317  dfcgra2  29320  sacgr  29321  angmgmaddcl  29373  f1otrge  29431  xmstrkgc  29445  colinearalglem1  29466  colinearalg  29470  axcgrtr  29475  axlowdimlem16  29517  axeuclidlem  29522  axcontlem4  29527  axcontlem7  29530  axcontlem12  29535  eengtrkg  29546  eengtrkge  29547  edglnl  29703  subgruhgredgd  29847  nbfusgrlevtxm2  29941  upgrwlkdvde  30305  crctcshwlkn0lem5  30385  crctcshwlkn0  30392  usgrwwlks2on  30529  umgrwwlks2on  30530  rusgrnumwwlks  30548  clwlkclwwlkfo  30582  3spthd  30759  frgr2wwlkeqm  30914  dlwwlknondlwlknonf1o  30948  numclwwlk5  30971  friendship  30982  grpomuldivass  31125  ablodivdiv4  31138  dipdi  31427  dipsubdi  31433  disjdsct  33278  archiabllem2c  33738  dvrcan5  33778  rloccring  33814  reofld  33886  eqgvscpbl  33893  qusvsval  33895  quslmod  33901  quslmhm  33902  ssmxidl  33981  ply1degltlss  34110  r1plmhm  34123  drgextlsp  34208  ccfldsrarelvec  34285  constrconj  34359  constrfin  34360  constrelextdg2  34361  pstmfval  34510  qqhval2lem  34595  qqhvq  34601  esumcvg  34700  sigaclcu  34731  measdivcst  34839  measdivcstALTV  34840  carsggect  34933  tgoldbachgtd  35274  bnj970  35560  bnj910  35561  erdszelem9  35933  cvmseu  36010  elmrsubrn  36254  r1peuqusdeg1  36377  cgrid2  36738  btwncomim  36748  btwnswapid  36752  trisegint  36763  cgrxfr  36790  btwnxfr  36791  brofs2  36812  brifs2  36813  endofsegid  36820  btwnconn1lem11  36832  btwnconn2  36837  segcon2  36840  seglemin  36848  segletr  36849  btwnsegle  36852  colinbtwnle  36853  broutsideof2  36857  btwnoutside  36860  broutsideof3  36861  outsideoftr  36864  outsidele  36867  ellines  36887  linethrueu  36891  nmulprop  36909  nadddi  36943  weiunpo  37223  unbdqndv2  37347  poimirlem28  38534  ftc1anc  38587  sdclem1  38645  sstotbnd2  38676  ismndo1  38775  zerdivemp1x  38849  isdrngo2  38860  iscringd  38900  lsmsat  40033  lfladdcl  40096  lflnegcl  40100  lflvscl  40102  lshpkrlem4  40138  lshpkrlem6  40140  ldualgrplem  40170  lduallmodlem  40177  latmassOLD  40254  latm12  40255  latm32  40256  latmrot  40257  latmmdiN  40259  latmmdir  40260  omlfh1N  40283  omlfh3N  40284  cvrnbtwn2  40300  cvlexchb1  40355  cvlexch3  40357  cvlexch4N  40358  cvlatexchb1  40359  cvlsupr2  40368  hlatjass  40395  hlatj12  40396  hlatj32  40397  cvrat  40447  atcvrj0  40453  cvrat2  40454  atltcvr  40460  atexchltN  40466  cvrat3  40467  cvrat4  40468  atbtwnexOLDN  40472  atbtwnex  40473  3dimlem3  40486  3dimlem3OLDN  40487  3at  40515  2atneat  40540  llncmp  40547  2at0mat0  40550  2atmat0  40551  islpln2a  40573  llncvrlpln  40583  lplncmp  40587  3atnelvolN  40611  4atlem11  40634  lplncvrlvol  40641  lvolcmp  40642  2atm2atN  40810  elpaddatriN  40828  elpadd2at2  40832  paddasslem8  40852  paddasslem17  40861  paddass  40863  padd12N  40864  paddssw1  40868  pmodlem2  40872  pmodN  40875  pmapjlln1  40880  atmod1i2  40884  pexmidlem2N  40996  pexmidlem7N  41001  pl42lem2N  41005  pl42lem3N  41006  pl42lem4N  41007  pl42N  41008  lhp2lt  41026  lhpm0atN  41054  lautlt  41116  lautcvr  41117  lautj  41118  lautm  41119  ltrneq2  41173  cdleme1b  41251  cdleme3b  41254  cdleme3c  41255  cdleme9b  41277  cdlemefs27cl  41438  cdleme42mN  41512  cdlemg4c  41637  trljco  41765  tgrpgrplem  41774  tendoplass  41808  tendodi1  41809  tendodi2  41810  erngplus2  41829  erngplus2-rN  41837  cdlemk36  41938  erngdvlem3  42015  erngdvlem3-rN  42023  dvaplusgv  42035  tendospass  42044  tendospdi1  42045  dvalveclem  42050  dialss  42071  dvhvaddass  42122  dvhopvsca  42127  dvhlveclem  42133  diblss  42195  diclss  42218  diclspsn  42219  cdlemn11pre  42235  dihmeetlem12N  42343  dihmeetlem16N  42347  dihmeetlem17N  42348  dvh4dimN  42472  lpolsatN  42513  lpolpolsatN  42514  dochpolN  42515  lclkr  42558  lclkrs  42564  lcfr  42610  lcmineqlem13  43059  aks6d1c1  43134  irrapxlem6  43787  jm2.26lem3  43961  mpaamn  44116  mendring  44148  mendlmod  44149  mendassa  44150  nnoeomeqom  44272  omabs2  44292  neicvgel1  45078  rfcnpre4  45994  fmuldfeq  46539  stoweidlem43  46997  stoweidlem52  47006  stoweidlem53  47007  stoweidlem56  47010  issmfgt  47710  issmfge  47724  tmachlem-franscan  47903  iccelpart  48459  prproropf1olem1  48529  fmtnoprmfac1  48594  fmtnoprmfac2  48596  isubgr3stgrlem2  49009  isubgr3stgrlem4  49011  grlimgrtrilem1  49043  copissgrp  49209  cznrng  49302  funcringcsetcALTV2lem9  49339  funcringcsetclem9ALTV  49362  idomcanl  49388  linccl  49470  lincsumscmcl  49489  ldepsprlem  49528  lincresunit3lem1  49535  itsclc0yqe  49817  resipos  50027  topdlat  50056  catprs  50063  endmndlem  50067  idmon  50072  idepi  50073  thincmon  50485  thincepi  50486  functhinclem1  50496  grptcmon  50645  grptcepi  50646  nellindf  50914