Theorem simpr3 1196

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

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

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 1089

This theorem is referenced by:  simpr13  1259  simpr23  1262  simpr33  1265  simp1r3  1271  simp2r3  1277  simp3r3  1283  3anandis  1471  funopsn  7182  fpr2g  7248  isopolem  7381  fr3nr  7807  sexp3  8194  suppfnss  8230  naddass  8752  dif1en  9226  elfir  9484  intrnfi  9485  fisupcl  9538  cnfcomlem  9768  ttrclss  9789  dmttrcl  9790  rnttrcl  9791  ttrclselem2  9795  ackbij1lem15  10302  pwfseqlem4a  10730  pwfseqlem4  10731  eluzuzle  12912  xlesubadd  13325  elioc2  13470  elico2  13471  elicc2  13472  fseq1p1m1  13658  ccatswrd  14716  pfxccat3a  14786  2cshw  14861  tanadd  16215  dvds2ln  16337  prmgaplem5  17102  prmgaplem8  17105  cshwsidrepsw  17141  ressress  17307  f1ovscpbl  17586  mreexexlem4d  17705  mreexexd  17706  2oppccomf  17785  fthmon  17994  fuccocl  18034  fucidcl  18035  invfuc  18044  initoeu2lem1  18081  curf2cl  18301  yonedalem4c  18347  yonedalem3  18350  pospo  18415  latjle12  18520  latjlej1  18523  latnlej2  18529  latlem12  18536  latmlem1  18539  latledi  18547  latjass  18553  latj12  18554  latj32  18555  latj13  18556  latj31  18557  latjrot  18558  latjjdi  18561  latjjdir  18562  latdisdlem  18566  prdssgrpd  18771  prdsmndd  18805  imasmnd2  18809  imasmnd  18810  frmdmnd  18894  grpsubadd  19068  grpaddsubass  19070  grpsubsub4  19073  grppnpcan2  19074  grpnpncan  19075  grpnnncan2  19077  imasgrp2  19095  imasgrp  19096  mulgnndir  19143  mulgnn0dir  19144  mulgnnass  19149  mulgnn0ass  19150  mulgass  19151  pwsmulg  19159  issubg2  19181  qusgrp  19226  kerf1ghm  19287  galcan  19344  gacan  19345  oppgmnd  19397  pmtrprfv  19495  pmtr3ncom  19517  psgnunilem3  19538  frgp0  19802  cmn32  19842  cmn12  19844  abladdsub  19854  ablsubaddsub  19856  ablsubsub23  19866  mulgdi  19868  mulgsubdi  19871  dprdss  20073  dprdf1o  20076  dprdsn  20080  dmdprdsplit  20091  pgpfac1lem5  20123  prdsrngd  20203  imasrng  20204  srgdilem  20219  ringdilem  20276  ringrng  20308  prdsringd  20344  imasring  20353  opprrng  20371  mulgass3  20379  dvrass  20434  dvrdir  20438  subrgunit  20618  issubrg2  20620  isdomn4  20738  abvdiv  20852  lss1  20959  lsssn0  20969  islss3  20980  prdslmodd  20990  islmhm2  21060  lspsolv  21168  lbsextlem4  21186  sralmod  21217  rnglidl1  21265  ipdi  21681  ipsubdir  21683  ipsubdi  21684  ipassr  21687  ipassr2  21688  isphld  21695  ocvlss  21713  sraassab  21911  sraassaOLD  21913  psrgrpOLD  22000  psrlmod  22003  psrring  22013  psrassa  22016  mpllsslem  22043  mamudm  22420  matring  22470  matassa  22471  ofco2  22478  scmatlss  22552  ma1repveval  22598  mdetunilem1  22639  mdetunilem9  22647  monmatcollpw  22806  iinopn  22929  restopnb  23204  subbascn  23283  hausnei2  23382  nrmsep2  23385  isnrm3  23388  t1sep  23399  regsep2  23405  dnsconst  23407  dfconn2  23448  dislly  23526  tx1stc  23679  qtophmeo  23846  filss  23882  infil  23892  fsubbas  23896  filssufilg  23940  hauspwpwf1  24016  cnextcn  24096  tmdcn2  24118  psmettri  24342  isxmet2d  24358  xmettri  24382  xmetres2  24392  bldisj  24429  blss2ps  24434  blss2  24435  xmstri2  24497  mstri2  24498  xmstri  24499  mstri  24500  xmstri3  24501  mstri3  24502  msrtri  24503  comet  24547  met2ndci  24556  ngprcan  24644  ngplcan  24645  ngpsubcan  24648  nmtri2  24661  nrgdsdi  24707  nrgdsdir  24708  nlmdsdi  24723  nlmdsdir  24724  blcvx  24839  iocopnst  24989  icccvx  25000  pi1grplem  25101  pi1xfrf  25105  pi1cof  25111  clmpm1dir  25155  cmodscmulexp  25174  cvsdiv  25184  cvsdivcl  25185  cphdivcl  25235  cphsubdir  25261  cphsubdi  25262  bcthlem5  25381  rrxcph  25445  volfiniun  25601  volcn  25660  itg1val2  25738  dvconst  25972  dvlip  26052  ftc1a  26098  ulmdvlem3  26463  ang180  26875  cvxcl  27046  scvxcvx  27047  sgmmul  27263  logexprlim  27287  dchrabl  27316  nosupbnd1  27777  noinfbnd1lem5  27790  noinfbnd1  27792  ssltsep  27853  addscom  28017  addsbday  28068  addsdi  28199  mulsass  28210  motgrp  28569  iscgra1  28836  cgrane2  28839  cgrane4  28841  cgrahl1  28842  cgrahl2  28843  cgracgr  28844  cgratr  28849  cgrabtwn  28852  cgrahl  28853  dfcgra2  28856  sacgr  28857  f1otrge  28898  xmstrkgc  28918  colinearalglem1  28939  colinearalg  28943  axcgrtr  28948  axlowdimlem16  28990  axeuclidlem  28995  axcontlem4  29000  axcontlem7  29003  axcontlem12  29008  eengtrkg  29019  eengtrkge  29020  edglnl  29178  subgruhgredgd  29319  nbfusgrlevtxm2  29413  upgrwlkdvde  29773  crctcshwlkn0lem5  29847  crctcshwlkn0  29854  umgrwwlks2on  29990  rusgrnumwwlks  30007  clwlkclwwlkfo  30041  3spthd  30208  frgr2wwlkeqm  30363  dlwwlknondlwlknonf1o  30397  numclwwlk5  30420  friendship  30431  grpomuldivass  30573  ablodivdiv4  30586  dipdi  30875  dipsubdi  30881  disjdsct  32714  omndmul2  33062  archiabllem2c  33175  dvrcan5  33216  rloccring  33242  reofld  33337  eqgvscpbl  33343  qusvsval  33345  quslmod  33351  quslmhm  33352  prmidlc  33441  ssdifidl  33450  ssmxidl  33467  ply1degltlss  33582  r1plmhm  33595  drgextlsp  33608  ccfldsrarelvec  33681  constrconj  33735  constrfin  33736  constrelextdg2  33737  pstmfval  33842  qqhval2lem  33927  qqhvq  33933  esumcvg  34050  sigaclcu  34081  measdivcst  34188  measdivcstALTV  34189  carsggect  34283  tgoldbachgtd  34639  bnj970  34923  bnj910  34924  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  36431  unbdqndv2  36477  poimirlem28  37608  ftc1anc  37661  sdclem1  37703  sstotbnd2  37734  ismndo1  37833  zerdivemp1x  37907  isdrngo2  37918  iscringd  37958  lsmsat  38964  lfladdcl  39027  lflnegcl  39031  lflvscl  39033  lshpkrlem4  39069  lshpkrlem6  39071  ldualgrplem  39101  lduallmodlem  39108  latmassOLD  39185  latm12  39186  latm32  39187  latmrot  39188  latmmdiN  39190  latmmdir  39191  omlfh1N  39214  omlfh3N  39215  cvrnbtwn2  39231  cvlexchb1  39286  cvlexch3  39288  cvlexch4N  39289  cvlatexchb1  39290  cvlsupr2  39299  hlatjass  39326  hlatj12  39327  hlatj32  39328  cvrat  39379  atcvrj0  39385  cvrat2  39386  atltcvr  39392  atexchltN  39398  cvrat3  39399  cvrat4  39400  atbtwnexOLDN  39404  atbtwnex  39405  3dimlem3  39418  3dimlem3OLDN  39419  3at  39447  2atneat  39472  llncmp  39479  2at0mat0  39482  2atmat0  39483  islpln2a  39505  llncvrlpln  39515  lplncmp  39519  3atnelvolN  39543  4atlem11  39566  lplncvrlvol  39573  lvolcmp  39574  2atm2atN  39742  elpaddatriN  39760  elpadd2at2  39764  paddasslem8  39784  paddasslem17  39793  paddass  39795  padd12N  39796  paddssw1  39800  pmodlem2  39804  pmodN  39807  pmapjlln1  39812  atmod1i2  39816  pexmidlem2N  39928  pexmidlem7N  39933  pl42lem2N  39937  pl42lem3N  39938  pl42lem4N  39939  pl42N  39940  lhp2lt  39958  lhpm0atN  39986  lautlt  40048  lautcvr  40049  lautj  40050  lautm  40051  ltrneq2  40105  cdleme1b  40183  cdleme3b  40186  cdleme3c  40187  cdleme9b  40209  cdlemefs27cl  40370  cdleme42mN  40444  cdlemg4c  40569  trljco  40697  tgrpgrplem  40706  tendoplass  40740  tendodi1  40741  tendodi2  40742  erngplus2  40761  erngplus2-rN  40769  cdlemk36  40870  erngdvlem3  40947  erngdvlem3-rN  40955  dvaplusgv  40967  tendospass  40976  tendospdi1  40977  dvalveclem  40982  dialss  41003  dvhvaddass  41054  dvhopvsca  41059  dvhlveclem  41065  diblss  41127  diclss  41150  diclspsn  41151  cdlemn11pre  41167  dihmeetlem12N  41275  dihmeetlem16N  41279  dihmeetlem17N  41280  dvh4dimN  41404  lpolsatN  41445  lpolpolsatN  41446  dochpolN  41447  lclkr  41490  lclkrs  41496  lcfr  41542  lcmineqlem13  41998  aks6d1c1  42073  irrapxlem6  42783  jm2.26lem3  42958  mpaamn  43113  mendring  43149  mendlmod  43150  mendassa  43151  nnoeomeqom  43274  omabs2  43294  neicvgel1  44081  rfcnpre4  44934  fmuldfeq  45504  stoweidlem43  45964  stoweidlem52  45973  stoweidlem53  45974  stoweidlem56  45977  issmfgt  46677  issmfge  46691  iccelpart  47307  prproropf1olem1  47377  fmtnoprmfac1  47439  fmtnoprmfac2  47441  grlimgrtrilem1  47818  copissgrp  47891  cznrng  47984  funcringcsetcALTV2lem9  48021  funcringcsetclem9ALTV  48044  linccl  48143  lincsumscmcl  48162  ldepsprlem  48201  lincresunit3lem1  48208  itsclc0yqe  48495  topdlat  48676  catprs  48678  endmndlem  48682  idmon  48683  idepi  48684  thincmon  48701  thincepi  48702  functhinclem1  48708  grptcmon  48763  grptcepi  48764