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  7151  funopsnOLD  7152  fpr2g  7217  isopolem  7353  fr3nr  7786  sexp3  8172  suppfnss  8209  naddass  8709  dif1en  9180  elfir  9410  intrnfi  9411  fisupcl  9465  cnfcomlem  9703  ttrclss  9724  dmttrcl  9725  rnttrcl  9726  ttrclselem2  9730  ackbij1lem15  10314  pwfseqlem4a  10749  pwfseqlem4  10750  eluzuzle  12977  xlesubadd  13396  elioc2  13543  elico2  13544  elicc2  13545  fseq1p1m1  13735  ccatswrd  14822  pfxccat3a  14891  2cshw  14968  tanadd  16340  dvds2ln  16464  prmgaplem5  17238  prmgaplem8  17241  cshwsidrepsw  17276  ressress  17430  f1ovscpbl  17703  mreexexlem4d  17826  mreexexd  17827  2oppccomf  17904  fthmon  18109  fuccocl  18147  fucidcl  18148  invfuc  18157  initoeu2lem1  18194  curf2cl  18410  yonedalem4c  18456  yonedalem3  18459  pospo  18522  latjle12  18629  latjlej1  18632  latnlej2  18638  latlem12  18645  latmlem1  18648  latledi  18656  latjass  18662  latj12  18663  latj32  18664  latj13  18665  latj31  18666  latjrot  18667  latjjdi  18670  latjjdir  18671  latdisdlem  18675  prdssgrpd  18927  prdsmndd  18969  imasmnd2  18973  imasmnd  18974  frmdmnd  19060  grpsubadd  19243  grpaddsubass  19245  grpsubsub4  19248  grppnpcan2  19249  grpnpncan  19250  grpnnncan2  19252  imasgrp2  19270  imasgrp  19271  mulgnndir  19318  mulgnn0dir  19319  mulgnnass  19324  mulgnn0ass  19325  mulgass  19326  pwsmulg  19334  issubg2  19357  qusgrp  19406  kerf1ghm  19466  galcan  19523  gacan  19524  oppgmnd  19573  pmtrprfv  19672  pmtr3ncom  19694  psgnunilem3  19715  frgp0  19979  cmn32  20019  cmn12  20021  abladdsub  20031  ablsubaddsub  20033  ablsubsub23  20043  mulgdi  20045  mulgsubdi  20048  dprdss  20250  dprdf1o  20253  dprdsn  20257  dmdprdsplit  20268  pgpfac1lem5  20300  omndmul2  20352  prdsrngd  20403  imasrng  20404  srgdilem  20423  ringdilem  20481  ringrng  20519  prdsringd  20555  imasring  20565  opprrng  20580  mulgass3  20588  dvrass  20643  dvrdir  20647  subrgunit  20847  issubrg2  20849  isdomn4  20972  abvdiv  21091  lss1  21218  lsssn0  21228  islss3  21239  prdslmodd  21249  islmhm2  21318  lspsolv  21426  lbsextlem4  21444  sralmod  21467  rnglidl1  21517  prmidlc  21634  ssdifidl  21646  ipdi  21951  ipsubdir  21953  ipsubdi  21954  ipassr  21957  ipassr2  21958  isphld  21965  ocvlss  21983  sraassab  22181  psrlmod  22272  psrring  22282  psrassa  22285  mpllsslem  22312  mamudm  22715  matring  22763  matassa  22764  ofco2  22771  scmatlss  22845  ma1repveval  22891  mdetunilem1  22932  mdetunilem9  22940  monmatcollpw  23102  iinopn  23225  restopnb  23498  subbascn  23577  hausnei2  23676  nrmsep2  23679  isnrm3  23682  t1sep  23693  regsep2  23699  dnsconst  23701  dfconn2  23742  dislly  23821  tx1stc  23974  qtophmeo  24141  filss  24177  infil  24187  fsubbas  24191  filssufilg  24235  hauspwpwf1  24311  cnextcn  24391  tmdcn2  24413  psmettri  24635  isxmet2d  24651  xmettri  24675  xmetres2  24685  bldisj  24722  blss2ps  24727  blss2  24728  xmstri2  24790  mstri2  24791  xmstri  24792  mstri  24793  xmstri3  24794  mstri3  24795  msrtri  24796  comet  24837  met2ndci  24846  ngprcan  24934  ngplcan  24935  ngpsubcan  24938  nmtri2  24951  nrgdsdi  24989  nrgdsdir  24990  nlmdsdi  25005  nlmdsdir  25006  blcvx  25122  iocopnst  25266  icccvx  25276  pi1grplem  25375  pi1xfrf  25379  pi1cof  25385  clmpm1dir  25429  cmodscmulexp  25448  cvsdiv  25458  cvsdivcl  25459  cphdivcl  25508  cphsubdir  25534  cphsubdi  25535  bcthlem5  25654  rrxcph  25718  volfiniun  25873  volcn  25932  itg1val2  26010  dvconst  26242  dvlip  26318  ftc1a  26362  ulmdvlem3  26734  ang180  27147  cvxcl  27317  scvxcvx  27318  sgmmul  27533  logexprlim  27557  dchrabl  27586  nosupbnd1  28076  noinfbnd1lem5  28089  noinfbnd1  28091  sltssep  28158  addscom  28357  addbday  28409  addsdi  28546  mulsass  28557  motgrp  29011  iscgra1  29322  cgrane2  29325  cgrane4  29327  cgrahl1  29328  cgrahl2  29329  cgracgr  29330  cgratr  29335  cgrabtwn  29339  cgrahl  29340  dfcgra2  29343  sacgr  29344  angmgmaddcl  29396  f1otrge  29454  xmstrkgc  29468  colinearalglem1  29489  colinearalg  29493  axcgrtr  29498  axlowdimlem16  29540  axeuclidlem  29545  axcontlem4  29550  axcontlem7  29553  axcontlem12  29558  eengtrkg  29569  eengtrkge  29570  edglnl  29726  subgruhgredgd  29870  nbfusgrlevtxm2  29964  upgrwlkdvde  30328  crctcshwlkn0lem5  30408  crctcshwlkn0  30415  usgrwwlks2on  30552  umgrwwlks2on  30553  rusgrnumwwlks  30571  clwlkclwwlkfo  30605  3spthd  30782  frgr2wwlkeqm  30937  dlwwlknondlwlknonf1o  30971  numclwwlk5  30994  friendship  31005  grpomuldivass  31148  ablodivdiv4  31161  dipdi  31450  dipsubdi  31456  disjdsct  33343  archiabllem2c  33802  dvrcan5  33842  rloccring  33878  reofld  33950  eqgvscpbl  33957  qusvsval  33959  quslmod  33965  quslmhm  33966  ssmxidl  34045  ply1degltlss  34174  r1plmhm  34187  drgextlsp  34272  ccfldsrarelvec  34349  constrconj  34423  constrfin  34424  constrelextdg2  34425  pstmfval  34574  qqhval2lem  34659  qqhvq  34665  esumcvg  34764  sigaclcu  34795  measdivcst  34903  measdivcstALTV  34904  carsggect  34996  tgoldbachgtd  35337  bnj970  35623  bnj910  35624  erdszelem9  36050  cvmseu  36127  elmrsubrn  36371  r1peuqusdeg1  36494  cgrid2  36860  btwncomim  36870  btwnswapid  36874  trisegint  36885  cgrxfr  36912  btwnxfr  36913  brofs2  36934  brifs2  36935  endofsegid  36942  btwnconn1lem11  36954  btwnconn2  36959  segcon2  36962  seglemin  36970  segletr  36971  btwnsegle  36974  colinbtwnle  36975  broutsideof2  36979  btwnoutside  36982  broutsideof3  36983  outsideoftr  36986  outsidele  36989  ellines  37009  linethrueu  37013  nmulprop  37031  nadddi  37065  weiunpo  37345  unbdqndv2  37469  poimirlem28  38659  ftc1anc  38712  sdclem1  38770  sstotbnd2  38801  ismndo1  38900  zerdivemp1x  38974  isdrngo2  38985  iscringd  39025  lsmsat  40158  lfladdcl  40221  lflnegcl  40225  lflvscl  40227  lshpkrlem4  40263  lshpkrlem6  40265  ldualgrplem  40295  lduallmodlem  40302  latmassOLD  40379  latm12  40380  latm32  40381  latmrot  40382  latmmdiN  40384  latmmdir  40385  omlfh1N  40408  omlfh3N  40409  cvrnbtwn2  40425  cvlexchb1  40480  cvlexch3  40482  cvlexch4N  40483  cvlatexchb1  40484  cvlsupr2  40493  hlatjass  40520  hlatj12  40521  hlatj32  40522  cvrat  40572  atcvrj0  40578  cvrat2  40579  atltcvr  40585  atexchltN  40591  cvrat3  40592  cvrat4  40593  atbtwnexOLDN  40597  atbtwnex  40598  3dimlem3  40611  3dimlem3OLDN  40612  3at  40640  2atneat  40665  llncmp  40672  2at0mat0  40675  2atmat0  40676  islpln2a  40698  llncvrlpln  40708  lplncmp  40712  3atnelvolN  40736  4atlem11  40759  lplncvrlvol  40766  lvolcmp  40767  2atm2atN  40935  elpaddatriN  40953  elpadd2at2  40957  paddasslem8  40977  paddasslem17  40986  paddass  40988  padd12N  40989  paddssw1  40993  pmodlem2  40997  pmodN  41000  pmapjlln1  41005  atmod1i2  41009  pexmidlem2N  41121  pexmidlem7N  41126  pl42lem2N  41130  pl42lem3N  41131  pl42lem4N  41132  pl42N  41133  lhp2lt  41151  lhpm0atN  41179  lautlt  41241  lautcvr  41242  lautj  41243  lautm  41244  ltrneq2  41298  cdleme1b  41376  cdleme3b  41379  cdleme3c  41380  cdleme9b  41402  cdlemefs27cl  41563  cdleme42mN  41637  cdlemg4c  41762  trljco  41890  tgrpgrplem  41899  tendoplass  41933  tendodi1  41934  tendodi2  41935  erngplus2  41954  erngplus2-rN  41962  cdlemk36  42063  erngdvlem3  42140  erngdvlem3-rN  42148  dvaplusgv  42160  tendospass  42169  tendospdi1  42170  dvalveclem  42175  dialss  42196  dvhvaddass  42247  dvhopvsca  42252  dvhlveclem  42258  diblss  42320  diclss  42343  diclspsn  42344  cdlemn11pre  42360  dihmeetlem12N  42468  dihmeetlem16N  42472  dihmeetlem17N  42473  dvh4dimN  42597  lpolsatN  42638  lpolpolsatN  42639  dochpolN  42640  lclkr  42683  lclkrs  42689  lcfr  42735  lcmineqlem13  43184  aks6d1c1  43259  irrapxlem6  43927  jm2.26lem3  44101  mpaamn  44251  mendring  44283  mendlmod  44284  mendassa  44285  nnoeomeqom  44407  omabs2  44427  neicvgel1  45212  rfcnpre4  46144  fmuldfeq  46688  stoweidlem43  47146  stoweidlem52  47155  stoweidlem53  47156  stoweidlem56  47159  issmfgt  47859  issmfge  47873  tmachlem-franscan  48052  iccelpart  48608  prproropf1olem1  48678  fmtnoprmfac1  48743  fmtnoprmfac2  48745  isubgr3stgrlem2  49158  isubgr3stgrlem4  49160  grlimgrtrilem1  49192  copissgrp  49358  cznrng  49451  funcringcsetcALTV2lem9  49488  funcringcsetclem9ALTV  49511  idomcanl  49537  linccl  49619  lincsumscmcl  49638  ldepsprlem  49677  lincresunit3lem1  49684  itsclc0yqe  49966  resipos  50182  topdlat  50211  catprs  50218  endmndlem  50222  idmon  50227  idepi  50228  thincmon  50661  thincepi  50662  functhinclem1  50672  grptcmon  50824  grptcepi  50825  nellindf  51138