Theorem simpr3 1198

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 1192	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  1261  simpr23  1264  simpr33  1267  simp1r3  1273  simp2r3  1279  simp3r3  1285  3anandis  1474  funopsn  7095  fpr2g  7159  isopolem  7293  fr3nr  7719  sexp3  8096  suppfnss  8132  naddass  8625  dif1en  9089  elfir  9321  intrnfi  9322  fisupcl  9376  cnfcomlem  9611  ttrclss  9632  dmttrcl  9633  rnttrcl  9634  ttrclselem2  9638  ackbij1lem15  10146  pwfseqlem4a  10575  pwfseqlem4  10576  eluzuzle  12788  xlesubadd  13206  elioc2  13353  elico2  13354  elicc2  13355  fseq1p1m1  13543  ccatswrd  14622  pfxccat3a  14691  2cshw  14766  tanadd  16125  dvds2ln  16249  prmgaplem5  17017  prmgaplem8  17020  cshwsidrepsw  17055  ressress  17208  f1ovscpbl  17481  mreexexlem4d  17604  mreexexd  17605  2oppccomf  17682  fthmon  17887  fuccocl  17925  fucidcl  17926  invfuc  17935  initoeu2lem1  17972  curf2cl  18188  yonedalem4c  18234  yonedalem3  18237  pospo  18300  latjle12  18407  latjlej1  18410  latnlej2  18416  latlem12  18423  latmlem1  18426  latledi  18434  latjass  18440  latj12  18441  latj32  18442  latj13  18443  latj31  18444  latjrot  18445  latjjdi  18448  latjjdir  18449  latdisdlem  18453  prdssgrpd  18692  prdsmndd  18729  imasmnd2  18733  imasmnd  18734  frmdmnd  18818  grpsubadd  18995  grpaddsubass  18997  grpsubsub4  19000  grppnpcan2  19001  grpnpncan  19002  grpnnncan2  19004  imasgrp2  19022  imasgrp  19023  mulgnndir  19070  mulgnn0dir  19071  mulgnnass  19076  mulgnn0ass  19077  mulgass  19078  pwsmulg  19086  issubg2  19108  qusgrp  19152  kerf1ghm  19213  galcan  19270  gacan  19271  oppgmnd  19320  pmtrprfv  19419  pmtr3ncom  19441  psgnunilem3  19462  frgp0  19726  cmn32  19766  cmn12  19768  abladdsub  19778  ablsubaddsub  19780  ablsubsub23  19790  mulgdi  19792  mulgsubdi  19795  dprdss  19997  dprdf1o  20000  dprdsn  20004  dmdprdsplit  20015  pgpfac1lem5  20047  omndmul2  20099  prdsrngd  20148  imasrng  20149  srgdilem  20164  ringdilem  20221  ringrng  20257  prdsringd  20291  imasring  20301  opprrng  20316  mulgass3  20324  dvrass  20379  dvrdir  20383  subrgunit  20558  issubrg2  20560  isdomn4  20684  abvdiv  20797  lss1  20924  lsssn0  20934  islss3  20945  prdslmodd  20955  islmhm2  21025  lspsolv  21133  lbsextlem4  21151  sralmod  21174  rnglidl1  21222  ipdi  21630  ipsubdir  21632  ipsubdi  21633  ipassr  21636  ipassr2  21637  isphld  21644  ocvlss  21662  sraassab  21858  psrlmod  21948  psrring  21958  psrassa  21961  mpllsslem  21988  mamudm  22370  matring  22418  matassa  22419  ofco2  22426  scmatlss  22500  ma1repveval  22546  mdetunilem1  22587  mdetunilem9  22595  monmatcollpw  22754  iinopn  22877  restopnb  23150  subbascn  23229  hausnei2  23328  nrmsep2  23331  isnrm3  23334  t1sep  23345  regsep2  23351  dnsconst  23353  dfconn2  23394  dislly  23472  tx1stc  23625  qtophmeo  23792  filss  23828  infil  23838  fsubbas  23842  filssufilg  23886  hauspwpwf1  23962  cnextcn  24042  tmdcn2  24064  psmettri  24286  isxmet2d  24302  xmettri  24326  xmetres2  24336  bldisj  24373  blss2ps  24378  blss2  24379  xmstri2  24441  mstri2  24442  xmstri  24443  mstri  24444  xmstri3  24445  mstri3  24446  msrtri  24447  comet  24488  met2ndci  24497  ngprcan  24585  ngplcan  24586  ngpsubcan  24589  nmtri2  24602  nrgdsdi  24640  nrgdsdir  24641  nlmdsdi  24656  nlmdsdir  24657  blcvx  24773  iocopnst  24917  icccvx  24927  pi1grplem  25026  pi1xfrf  25030  pi1cof  25036  clmpm1dir  25080  cmodscmulexp  25099  cvsdiv  25109  cvsdivcl  25110  cphdivcl  25159  cphsubdir  25185  cphsubdi  25186  bcthlem5  25305  rrxcph  25369  volfiniun  25524  volcn  25583  itg1val2  25661  dvconst  25894  dvlip  25970  ftc1a  26014  ulmdvlem3  26380  ang180  26791  cvxcl  26962  scvxcvx  26963  sgmmul  27178  logexprlim  27202  dchrabl  27231  nosupbnd1  27692  noinfbnd1lem5  27705  noinfbnd1  27707  sltssep  27773  addscom  27972  addbday  28024  addsdi  28161  mulsass  28172  motgrp  28625  iscgra1  28892  cgrane2  28895  cgrane4  28897  cgrahl1  28898  cgrahl2  28899  cgracgr  28900  cgratr  28905  cgrabtwn  28908  cgrahl  28909  dfcgra2  28912  sacgr  28913  f1otrge  28954  xmstrkgc  28968  colinearalglem1  28989  colinearalg  28993  axcgrtr  28998  axlowdimlem16  29040  axeuclidlem  29045  axcontlem4  29050  axcontlem7  29053  axcontlem12  29058  eengtrkg  29069  eengtrkge  29070  edglnl  29226  subgruhgredgd  29367  nbfusgrlevtxm2  29461  upgrwlkdvde  29820  crctcshwlkn0lem5  29897  crctcshwlkn0  29904  usgrwwlks2on  30041  umgrwwlks2on  30042  rusgrnumwwlks  30060  clwlkclwwlkfo  30094  3spthd  30261  frgr2wwlkeqm  30416  dlwwlknondlwlknonf1o  30450  numclwwlk5  30473  friendship  30484  grpomuldivass  30627  ablodivdiv4  30640  dipdi  30929  dipsubdi  30935  disjdsct  32791  archiabllem2c  33271  dvrcan5  33312  rloccring  33346  reofld  33418  eqgvscpbl  33425  qusvsval  33427  quslmod  33433  quslmhm  33434  prmidlc  33523  ssdifidl  33532  ssmxidl  33549  ply1degltlss  33671  r1plmhm  33685  drgextlsp  33753  ccfldsrarelvec  33831  constrconj  33905  constrfin  33906  constrelextdg2  33907  pstmfval  34056  qqhval2lem  34141  qqhvq  34147  esumcvg  34246  sigaclcu  34277  measdivcst  34384  measdivcstALTV  34385  carsggect  34478  tgoldbachgtd  34822  bnj970  35105  bnj910  35106  erdszelem9  35397  cvmseu  35474  elmrsubrn  35718  r1peuqusdeg1  35841  cgrid2  36201  btwncomim  36211  btwnswapid  36215  trisegint  36226  cgrxfr  36253  btwnxfr  36254  brofs2  36275  brifs2  36276  endofsegid  36283  btwnconn1lem11  36295  btwnconn2  36300  segcon2  36303  seglemin  36311  segletr  36312  btwnsegle  36315  colinbtwnle  36316  broutsideof2  36320  btwnoutside  36323  broutsideof3  36324  outsideoftr  36327  outsidele  36330  ellines  36350  linethrueu  36354  weiunpo  36663  unbdqndv2  36787  poimirlem28  37983  ftc1anc  38036  sdclem1  38078  sstotbnd2  38109  ismndo1  38208  zerdivemp1x  38282  isdrngo2  38293  iscringd  38333  lsmsat  39468  lfladdcl  39531  lflnegcl  39535  lflvscl  39537  lshpkrlem4  39573  lshpkrlem6  39575  ldualgrplem  39605  lduallmodlem  39612  latmassOLD  39689  latm12  39690  latm32  39691  latmrot  39692  latmmdiN  39694  latmmdir  39695  omlfh1N  39718  omlfh3N  39719  cvrnbtwn2  39735  cvlexchb1  39790  cvlexch3  39792  cvlexch4N  39793  cvlatexchb1  39794  cvlsupr2  39803  hlatjass  39830  hlatj12  39831  hlatj32  39832  cvrat  39882  atcvrj0  39888  cvrat2  39889  atltcvr  39895  atexchltN  39901  cvrat3  39902  cvrat4  39903  atbtwnexOLDN  39907  atbtwnex  39908  3dimlem3  39921  3dimlem3OLDN  39922  3at  39950  2atneat  39975  llncmp  39982  2at0mat0  39985  2atmat0  39986  islpln2a  40008  llncvrlpln  40018  lplncmp  40022  3atnelvolN  40046  4atlem11  40069  lplncvrlvol  40076  lvolcmp  40077  2atm2atN  40245  elpaddatriN  40263  elpadd2at2  40267  paddasslem8  40287  paddasslem17  40296  paddass  40298  padd12N  40299  paddssw1  40303  pmodlem2  40307  pmodN  40310  pmapjlln1  40315  atmod1i2  40319  pexmidlem2N  40431  pexmidlem7N  40436  pl42lem2N  40440  pl42lem3N  40441  pl42lem4N  40442  pl42N  40443  lhp2lt  40461  lhpm0atN  40489  lautlt  40551  lautcvr  40552  lautj  40553  lautm  40554  ltrneq2  40608  cdleme1b  40686  cdleme3b  40689  cdleme3c  40690  cdleme9b  40712  cdlemefs27cl  40873  cdleme42mN  40947  cdlemg4c  41072  trljco  41200  tgrpgrplem  41209  tendoplass  41243  tendodi1  41244  tendodi2  41245  erngplus2  41264  erngplus2-rN  41272  cdlemk36  41373  erngdvlem3  41450  erngdvlem3-rN  41458  dvaplusgv  41470  tendospass  41479  tendospdi1  41480  dvalveclem  41485  dialss  41506  dvhvaddass  41557  dvhopvsca  41562  dvhlveclem  41568  diblss  41630  diclss  41653  diclspsn  41654  cdlemn11pre  41670  dihmeetlem12N  41778  dihmeetlem16N  41782  dihmeetlem17N  41783  dvh4dimN  41907  lpolsatN  41948  lpolpolsatN  41949  dochpolN  41950  lclkr  41993  lclkrs  41999  lcfr  42045  lcmineqlem13  42494  aks6d1c1  42569  irrapxlem6  43273  jm2.26lem3  43447  mpaamn  43602  mendring  43634  mendlmod  43635  mendassa  43636  nnoeomeqom  43758  omabs2  43778  neicvgel1  44564  rfcnpre4  45483  fmuldfeq  46031  stoweidlem43  46489  stoweidlem52  46498  stoweidlem53  46499  stoweidlem56  46502  issmfgt  47202  issmfge  47216  iccelpart  47905  prproropf1olem1  47975  fmtnoprmfac1  48040  fmtnoprmfac2  48042  isubgr3stgrlem2  48455  isubgr3stgrlem4  48457  grlimgrtrilem1  48489  copissgrp  48656  cznrng  48749  funcringcsetcALTV2lem9  48786  funcringcsetclem9ALTV  48809  linccl  48902  lincsumscmcl  48921  ldepsprlem  48960  lincresunit3lem1  48967  itsclc0yqe  49249  resipos  49462  topdlat  49491  catprs  49498  endmndlem  49502  idmon  49507  idepi  49508  thincmon  49920  thincepi  49921  functhinclem1  49931  grptcmon  50080  grptcepi  50081