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  7081  fpr2g  7145  isopolem  7279  fr3nr  7705  sexp3  8083  suppfnss  8119  naddass  8611  dif1en  9071  elfir  9299  intrnfi  9300  fisupcl  9354  cnfcomlem  9589  ttrclss  9610  dmttrcl  9611  rnttrcl  9612  ttrclselem2  9616  ackbij1lem15  10121  pwfseqlem4a  10549  pwfseqlem4  10550  eluzuzle  12738  xlesubadd  13159  elioc2  13306  elico2  13307  elicc2  13308  fseq1p1m1  13495  ccatswrd  14573  pfxccat3a  14642  2cshw  14717  tanadd  16073  dvds2ln  16197  prmgaplem5  16964  prmgaplem8  16967  cshwsidrepsw  17002  ressress  17155  f1ovscpbl  17427  mreexexlem4d  17550  mreexexd  17551  2oppccomf  17628  fthmon  17833  fuccocl  17871  fucidcl  17872  invfuc  17881  initoeu2lem1  17918  curf2cl  18134  yonedalem4c  18180  yonedalem3  18183  pospo  18246  latjle12  18353  latjlej1  18356  latnlej2  18362  latlem12  18369  latmlem1  18372  latledi  18380  latjass  18386  latj12  18387  latj32  18388  latj13  18389  latj31  18390  latjrot  18391  latjjdi  18394  latjjdir  18395  latdisdlem  18399  prdssgrpd  18638  prdsmndd  18675  imasmnd2  18679  imasmnd  18680  frmdmnd  18764  grpsubadd  18938  grpaddsubass  18940  grpsubsub4  18943  grppnpcan2  18944  grpnpncan  18945  grpnnncan2  18947  imasgrp2  18965  imasgrp  18966  mulgnndir  19013  mulgnn0dir  19014  mulgnnass  19019  mulgnn0ass  19020  mulgass  19021  pwsmulg  19029  issubg2  19051  qusgrp  19096  kerf1ghm  19157  galcan  19214  gacan  19215  oppgmnd  19264  pmtrprfv  19363  pmtr3ncom  19385  psgnunilem3  19406  frgp0  19670  cmn32  19710  cmn12  19712  abladdsub  19722  ablsubaddsub  19724  ablsubsub23  19734  mulgdi  19736  mulgsubdi  19739  dprdss  19941  dprdf1o  19944  dprdsn  19948  dmdprdsplit  19959  pgpfac1lem5  19991  omndmul2  20043  prdsrngd  20092  imasrng  20093  srgdilem  20108  ringdilem  20165  ringrng  20201  prdsringd  20237  imasring  20246  opprrng  20261  mulgass3  20269  dvrass  20324  dvrdir  20328  subrgunit  20503  issubrg2  20505  isdomn4  20629  abvdiv  20742  lss1  20869  lsssn0  20879  islss3  20890  prdslmodd  20900  islmhm2  20970  lspsolv  21078  lbsextlem4  21096  sralmod  21119  rnglidl1  21167  ipdi  21575  ipsubdir  21577  ipsubdi  21578  ipassr  21581  ipassr2  21582  isphld  21589  ocvlss  21607  sraassab  21803  sraassaOLD  21805  psrgrpOLD  21892  psrlmod  21895  psrring  21905  psrassa  21908  mpllsslem  21935  mamudm  22308  matring  22356  matassa  22357  ofco2  22364  scmatlss  22438  ma1repveval  22484  mdetunilem1  22525  mdetunilem9  22533  monmatcollpw  22692  iinopn  22815  restopnb  23088  subbascn  23167  hausnei2  23266  nrmsep2  23269  isnrm3  23272  t1sep  23283  regsep2  23289  dnsconst  23291  dfconn2  23332  dislly  23410  tx1stc  23563  qtophmeo  23730  filss  23766  infil  23776  fsubbas  23780  filssufilg  23824  hauspwpwf1  23900  cnextcn  23980  tmdcn2  24002  psmettri  24224  isxmet2d  24240  xmettri  24264  xmetres2  24274  bldisj  24311  blss2ps  24316  blss2  24317  xmstri2  24379  mstri2  24380  xmstri  24381  mstri  24382  xmstri3  24383  mstri3  24384  msrtri  24385  comet  24426  met2ndci  24435  ngprcan  24523  ngplcan  24524  ngpsubcan  24527  nmtri2  24540  nrgdsdi  24578  nrgdsdir  24579  nlmdsdi  24594  nlmdsdir  24595  blcvx  24711  iocopnst  24862  icccvx  24873  pi1grplem  24974  pi1xfrf  24978  pi1cof  24984  clmpm1dir  25028  cmodscmulexp  25047  cvsdiv  25057  cvsdivcl  25058  cphdivcl  25107  cphsubdir  25133  cphsubdi  25134  bcthlem5  25253  rrxcph  25317  volfiniun  25473  volcn  25532  itg1val2  25610  dvconst  25843  dvlip  25923  ftc1a  25969  ulmdvlem3  26336  ang180  26749  cvxcl  26920  scvxcvx  26921  sgmmul  27137  logexprlim  27161  dchrabl  27190  nosupbnd1  27651  noinfbnd1lem5  27664  noinfbnd1  27666  ssltsep  27728  addscom  27907  addsbday  27958  addsdi  28092  mulsass  28103  motgrp  28519  iscgra1  28786  cgrane2  28789  cgrane4  28791  cgrahl1  28792  cgrahl2  28793  cgracgr  28794  cgratr  28799  cgrabtwn  28802  cgrahl  28803  dfcgra2  28806  sacgr  28807  f1otrge  28848  xmstrkgc  28862  colinearalglem1  28882  colinearalg  28886  axcgrtr  28891  axlowdimlem16  28933  axeuclidlem  28938  axcontlem4  28943  axcontlem7  28946  axcontlem12  28951  eengtrkg  28962  eengtrkge  28963  edglnl  29119  subgruhgredgd  29260  nbfusgrlevtxm2  29354  upgrwlkdvde  29713  crctcshwlkn0lem5  29790  crctcshwlkn0  29797  umgrwwlks2on  29933  rusgrnumwwlks  29950  clwlkclwwlkfo  29984  3spthd  30151  frgr2wwlkeqm  30306  dlwwlknondlwlknonf1o  30340  numclwwlk5  30363  friendship  30374  grpomuldivass  30516  ablodivdiv4  30529  dipdi  30818  dipsubdi  30824  disjdsct  32679  archiabllem2c  33159  dvrcan5  33198  rloccring  33232  reofld  33303  eqgvscpbl  33310  qusvsval  33312  quslmod  33318  quslmhm  33319  prmidlc  33408  ssdifidl  33417  ssmxidl  33434  ply1degltlss  33552  r1plmhm  33565  drgextlsp  33601  ccfldsrarelvec  33679  constrconj  33753  constrfin  33754  constrelextdg2  33755  pstmfval  33904  qqhval2lem  33989  qqhvq  33995  esumcvg  34094  sigaclcu  34125  measdivcst  34232  measdivcstALTV  34233  carsggect  34326  tgoldbachgtd  34670  bnj970  34954  bnj910  34955  erdszelem9  35231  cvmseu  35308  elmrsubrn  35552  r1peuqusdeg1  35675  cgrid2  36036  btwncomim  36046  btwnswapid  36050  trisegint  36061  cgrxfr  36088  btwnxfr  36089  brofs2  36110  brifs2  36111  endofsegid  36118  btwnconn1lem11  36130  btwnconn2  36135  segcon2  36138  seglemin  36146  segletr  36147  btwnsegle  36150  colinbtwnle  36151  broutsideof2  36155  btwnoutside  36158  broutsideof3  36159  outsideoftr  36162  outsidele  36165  ellines  36185  linethrueu  36189  weiunpo  36498  unbdqndv2  36544  poimirlem28  37687  ftc1anc  37740  sdclem1  37782  sstotbnd2  37813  ismndo1  37912  zerdivemp1x  37986  isdrngo2  37997  iscringd  38037  lsmsat  39046  lfladdcl  39109  lflnegcl  39113  lflvscl  39115  lshpkrlem4  39151  lshpkrlem6  39153  ldualgrplem  39183  lduallmodlem  39190  latmassOLD  39267  latm12  39268  latm32  39269  latmrot  39270  latmmdiN  39272  latmmdir  39273  omlfh1N  39296  omlfh3N  39297  cvrnbtwn2  39313  cvlexchb1  39368  cvlexch3  39370  cvlexch4N  39371  cvlatexchb1  39372  cvlsupr2  39381  hlatjass  39408  hlatj12  39409  hlatj32  39410  cvrat  39460  atcvrj0  39466  cvrat2  39467  atltcvr  39473  atexchltN  39479  cvrat3  39480  cvrat4  39481  atbtwnexOLDN  39485  atbtwnex  39486  3dimlem3  39499  3dimlem3OLDN  39500  3at  39528  2atneat  39553  llncmp  39560  2at0mat0  39563  2atmat0  39564  islpln2a  39586  llncvrlpln  39596  lplncmp  39600  3atnelvolN  39624  4atlem11  39647  lplncvrlvol  39654  lvolcmp  39655  2atm2atN  39823  elpaddatriN  39841  elpadd2at2  39845  paddasslem8  39865  paddasslem17  39874  paddass  39876  padd12N  39877  paddssw1  39881  pmodlem2  39885  pmodN  39888  pmapjlln1  39893  atmod1i2  39897  pexmidlem2N  40009  pexmidlem7N  40014  pl42lem2N  40018  pl42lem3N  40019  pl42lem4N  40020  pl42N  40021  lhp2lt  40039  lhpm0atN  40067  lautlt  40129  lautcvr  40130  lautj  40131  lautm  40132  ltrneq2  40186  cdleme1b  40264  cdleme3b  40267  cdleme3c  40268  cdleme9b  40290  cdlemefs27cl  40451  cdleme42mN  40525  cdlemg4c  40650  trljco  40778  tgrpgrplem  40787  tendoplass  40821  tendodi1  40822  tendodi2  40823  erngplus2  40842  erngplus2-rN  40850  cdlemk36  40951  erngdvlem3  41028  erngdvlem3-rN  41036  dvaplusgv  41048  tendospass  41057  tendospdi1  41058  dvalveclem  41063  dialss  41084  dvhvaddass  41135  dvhopvsca  41140  dvhlveclem  41146  diblss  41208  diclss  41231  diclspsn  41232  cdlemn11pre  41248  dihmeetlem12N  41356  dihmeetlem16N  41360  dihmeetlem17N  41361  dvh4dimN  41485  lpolsatN  41526  lpolpolsatN  41527  dochpolN  41528  lclkr  41571  lclkrs  41577  lcfr  41623  lcmineqlem13  42073  aks6d1c1  42148  irrapxlem6  42859  jm2.26lem3  43033  mpaamn  43188  mendring  43220  mendlmod  43221  mendassa  43222  nnoeomeqom  43344  omabs2  43364  neicvgel1  44151  rfcnpre4  45070  fmuldfeq  45622  stoweidlem43  46080  stoweidlem52  46089  stoweidlem53  46090  stoweidlem56  46093  issmfgt  46793  issmfge  46807  iccelpart  47463  prproropf1olem1  47533  fmtnoprmfac1  47595  fmtnoprmfac2  47597  isubgr3stgrlem2  47997  isubgr3stgrlem4  47999  grlimgrtrilem1  48031  copissgrp  48198  cznrng  48291  funcringcsetcALTV2lem9  48328  funcringcsetclem9ALTV  48351  linccl  48445  lincsumscmcl  48464  ldepsprlem  48503  lincresunit3lem1  48510  itsclc0yqe  48792  resipos  49005  topdlat  49034  catprs  49042  endmndlem  49046  idmon  49051  idepi  49052  thincmon  49464  thincepi  49465  functhinclem1  49475  grptcmon  49624  grptcepi  49625