Theorem simpr3 1197

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  simpr13  1260  simpr23  1263  simpr33  1266  simp1r3  1272  simp2r3  1278  simp3r3  1284  3anandis  1473  funopsn  7137  fpr2g  7202  isopolem  7337  fr3nr  7764  sexp3  8150  suppfnss  8186  naddass  8706  dif1en  9172  elfir  9425  intrnfi  9426  fisupcl  9480  cnfcomlem  9711  ttrclss  9732  dmttrcl  9733  rnttrcl  9734  ttrclselem2  9738  ackbij1lem15  10245  pwfseqlem4a  10673  pwfseqlem4  10674  eluzuzle  12859  xlesubadd  13277  elioc2  13424  elico2  13425  elicc2  13426  fseq1p1m1  13613  ccatswrd  14684  pfxccat3a  14754  2cshw  14829  tanadd  16183  dvds2ln  16306  prmgaplem5  17073  prmgaplem8  17076  cshwsidrepsw  17111  ressress  17266  f1ovscpbl  17538  mreexexlem4d  17657  mreexexd  17658  2oppccomf  17735  fthmon  17940  fuccocl  17978  fucidcl  17979  invfuc  17988  initoeu2lem1  18025  curf2cl  18241  yonedalem4c  18287  yonedalem3  18290  pospo  18353  latjle12  18458  latjlej1  18461  latnlej2  18467  latlem12  18474  latmlem1  18477  latledi  18485  latjass  18491  latj12  18492  latj32  18493  latj13  18494  latj31  18495  latjrot  18496  latjjdi  18499  latjjdir  18500  latdisdlem  18504  prdssgrpd  18709  prdsmndd  18746  imasmnd2  18750  imasmnd  18751  frmdmnd  18835  grpsubadd  19009  grpaddsubass  19011  grpsubsub4  19014  grppnpcan2  19015  grpnpncan  19016  grpnnncan2  19018  imasgrp2  19036  imasgrp  19037  mulgnndir  19084  mulgnn0dir  19085  mulgnnass  19090  mulgnn0ass  19091  mulgass  19092  pwsmulg  19100  issubg2  19122  qusgrp  19167  kerf1ghm  19228  galcan  19285  gacan  19286  oppgmnd  19335  pmtrprfv  19432  pmtr3ncom  19454  psgnunilem3  19475  frgp0  19739  cmn32  19779  cmn12  19781  abladdsub  19791  ablsubaddsub  19793  ablsubsub23  19803  mulgdi  19805  mulgsubdi  19808  dprdss  20010  dprdf1o  20013  dprdsn  20017  dmdprdsplit  20028  pgpfac1lem5  20060  prdsrngd  20134  imasrng  20135  srgdilem  20150  ringdilem  20207  ringrng  20243  prdsringd  20279  imasring  20288  opprrng  20303  mulgass3  20311  dvrass  20366  dvrdir  20370  subrgunit  20548  issubrg2  20550  isdomn4  20674  abvdiv  20787  lss1  20893  lsssn0  20903  islss3  20914  prdslmodd  20924  islmhm2  20994  lspsolv  21102  lbsextlem4  21120  sralmod  21143  rnglidl1  21191  ipdi  21598  ipsubdir  21600  ipsubdi  21601  ipassr  21604  ipassr2  21605  isphld  21612  ocvlss  21630  sraassab  21826  sraassaOLD  21828  psrgrpOLD  21915  psrlmod  21918  psrring  21928  psrassa  21931  mpllsslem  21958  mamudm  22331  matring  22379  matassa  22380  ofco2  22387  scmatlss  22461  ma1repveval  22507  mdetunilem1  22548  mdetunilem9  22556  monmatcollpw  22715  iinopn  22838  restopnb  23111  subbascn  23190  hausnei2  23289  nrmsep2  23292  isnrm3  23295  t1sep  23306  regsep2  23312  dnsconst  23314  dfconn2  23355  dislly  23433  tx1stc  23586  qtophmeo  23753  filss  23789  infil  23799  fsubbas  23803  filssufilg  23847  hauspwpwf1  23923  cnextcn  24003  tmdcn2  24025  psmettri  24248  isxmet2d  24264  xmettri  24288  xmetres2  24298  bldisj  24335  blss2ps  24340  blss2  24341  xmstri2  24403  mstri2  24404  xmstri  24405  mstri  24406  xmstri3  24407  mstri3  24408  msrtri  24409  comet  24450  met2ndci  24459  ngprcan  24547  ngplcan  24548  ngpsubcan  24551  nmtri2  24564  nrgdsdi  24602  nrgdsdir  24603  nlmdsdi  24618  nlmdsdir  24619  blcvx  24735  iocopnst  24886  icccvx  24897  pi1grplem  24998  pi1xfrf  25002  pi1cof  25008  clmpm1dir  25052  cmodscmulexp  25071  cvsdiv  25081  cvsdivcl  25082  cphdivcl  25132  cphsubdir  25158  cphsubdi  25159  bcthlem5  25278  rrxcph  25342  volfiniun  25498  volcn  25557  itg1val2  25635  dvconst  25868  dvlip  25948  ftc1a  25994  ulmdvlem3  26361  ang180  26774  cvxcl  26945  scvxcvx  26946  sgmmul  27162  logexprlim  27186  dchrabl  27215  nosupbnd1  27676  noinfbnd1lem5  27689  noinfbnd1  27691  ssltsep  27752  addscom  27916  addsbday  27967  addsdi  28098  mulsass  28109  motgrp  28468  iscgra1  28735  cgrane2  28738  cgrane4  28740  cgrahl1  28741  cgrahl2  28742  cgracgr  28743  cgratr  28748  cgrabtwn  28751  cgrahl  28752  dfcgra2  28755  sacgr  28756  f1otrge  28797  xmstrkgc  28811  colinearalglem1  28831  colinearalg  28835  axcgrtr  28840  axlowdimlem16  28882  axeuclidlem  28887  axcontlem4  28892  axcontlem7  28895  axcontlem12  28900  eengtrkg  28911  eengtrkge  28912  edglnl  29068  subgruhgredgd  29209  nbfusgrlevtxm2  29303  upgrwlkdvde  29665  crctcshwlkn0lem5  29742  crctcshwlkn0  29749  umgrwwlks2on  29885  rusgrnumwwlks  29902  clwlkclwwlkfo  29936  3spthd  30103  frgr2wwlkeqm  30258  dlwwlknondlwlknonf1o  30292  numclwwlk5  30315  friendship  30326  grpomuldivass  30468  ablodivdiv4  30481  dipdi  30770  dipsubdi  30776  disjdsct  32626  omndmul2  33026  archiabllem2c  33139  dvrcan5  33177  rloccring  33211  reofld  33305  eqgvscpbl  33311  qusvsval  33313  quslmod  33319  quslmhm  33320  prmidlc  33409  ssdifidl  33418  ssmxidl  33435  ply1degltlss  33552  r1plmhm  33565  drgextlsp  33579  ccfldsrarelvec  33658  constrconj  33725  constrfin  33726  constrelextdg2  33727  pstmfval  33873  qqhval2lem  33958  qqhvq  33964  esumcvg  34063  sigaclcu  34094  measdivcst  34201  measdivcstALTV  34202  carsggect  34296  tgoldbachgtd  34640  bnj970  34924  bnj910  34925  erdszelem9  35167  cvmseu  35244  elmrsubrn  35488  r1peuqusdeg1  35611  cgrid2  35967  btwncomim  35977  btwnswapid  35981  trisegint  35992  cgrxfr  36019  btwnxfr  36020  brofs2  36041  brifs2  36042  endofsegid  36049  btwnconn1lem11  36061  btwnconn2  36066  segcon2  36069  seglemin  36077  segletr  36078  btwnsegle  36081  colinbtwnle  36082  broutsideof2  36086  btwnoutside  36089  broutsideof3  36090  outsideoftr  36093  outsidele  36096  ellines  36116  linethrueu  36120  weiunpo  36429  unbdqndv2  36475  poimirlem28  37618  ftc1anc  37671  sdclem1  37713  sstotbnd2  37744  ismndo1  37843  zerdivemp1x  37917  isdrngo2  37928  iscringd  37968  lsmsat  38972  lfladdcl  39035  lflnegcl  39039  lflvscl  39041  lshpkrlem4  39077  lshpkrlem6  39079  ldualgrplem  39109  lduallmodlem  39116  latmassOLD  39193  latm12  39194  latm32  39195  latmrot  39196  latmmdiN  39198  latmmdir  39199  omlfh1N  39222  omlfh3N  39223  cvrnbtwn2  39239  cvlexchb1  39294  cvlexch3  39296  cvlexch4N  39297  cvlatexchb1  39298  cvlsupr2  39307  hlatjass  39334  hlatj12  39335  hlatj32  39336  cvrat  39387  atcvrj0  39393  cvrat2  39394  atltcvr  39400  atexchltN  39406  cvrat3  39407  cvrat4  39408  atbtwnexOLDN  39412  atbtwnex  39413  3dimlem3  39426  3dimlem3OLDN  39427  3at  39455  2atneat  39480  llncmp  39487  2at0mat0  39490  2atmat0  39491  islpln2a  39513  llncvrlpln  39523  lplncmp  39527  3atnelvolN  39551  4atlem11  39574  lplncvrlvol  39581  lvolcmp  39582  2atm2atN  39750  elpaddatriN  39768  elpadd2at2  39772  paddasslem8  39792  paddasslem17  39801  paddass  39803  padd12N  39804  paddssw1  39808  pmodlem2  39812  pmodN  39815  pmapjlln1  39820  atmod1i2  39824  pexmidlem2N  39936  pexmidlem7N  39941  pl42lem2N  39945  pl42lem3N  39946  pl42lem4N  39947  pl42N  39948  lhp2lt  39966  lhpm0atN  39994  lautlt  40056  lautcvr  40057  lautj  40058  lautm  40059  ltrneq2  40113  cdleme1b  40191  cdleme3b  40194  cdleme3c  40195  cdleme9b  40217  cdlemefs27cl  40378  cdleme42mN  40452  cdlemg4c  40577  trljco  40705  tgrpgrplem  40714  tendoplass  40748  tendodi1  40749  tendodi2  40750  erngplus2  40769  erngplus2-rN  40777  cdlemk36  40878  erngdvlem3  40955  erngdvlem3-rN  40963  dvaplusgv  40975  tendospass  40984  tendospdi1  40985  dvalveclem  40990  dialss  41011  dvhvaddass  41062  dvhopvsca  41067  dvhlveclem  41073  diblss  41135  diclss  41158  diclspsn  41159  cdlemn11pre  41175  dihmeetlem12N  41283  dihmeetlem16N  41287  dihmeetlem17N  41288  dvh4dimN  41412  lpolsatN  41453  lpolpolsatN  41454  dochpolN  41455  lclkr  41498  lclkrs  41504  lcfr  41550  lcmineqlem13  42000  aks6d1c1  42075  irrapxlem6  42797  jm2.26lem3  42972  mpaamn  43127  mendring  43159  mendlmod  43160  mendassa  43161  nnoeomeqom  43283  omabs2  43303  neicvgel1  44090  rfcnpre4  45006  fmuldfeq  45560  stoweidlem43  46020  stoweidlem52  46029  stoweidlem53  46030  stoweidlem56  46033  issmfgt  46733  issmfge  46747  iccelpart  47395  prproropf1olem1  47465  fmtnoprmfac1  47527  fmtnoprmfac2  47529  isubgr3stgrlem2  47927  isubgr3stgrlem4  47929  grlimgrtrilem1  47954  copissgrp  48091  cznrng  48184  funcringcsetcALTV2lem9  48221  funcringcsetclem9ALTV  48244  linccl  48338  lincsumscmcl  48357  ldepsprlem  48396  lincresunit3lem1  48403  itsclc0yqe  48689  resipos  48897  topdlat  48926  catprs  48934  endmndlem  48938  idmon  48943  idepi  48944  thincmon  49267  thincepi  49268  functhinclem1  49278  grptcmon  49418  grptcepi  49419