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 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  1260  simpr23  1263  simpr33  1266  simp1r3  1272  simp2r3  1278  simp3r3  1284  3anandis  1473  funopsn  7168  fpr2g  7231  isopolem  7365  fr3nr  7792  sexp3  8178  suppfnss  8214  naddass  8734  dif1en  9200  elfir  9455  intrnfi  9456  fisupcl  9509  cnfcomlem  9739  ttrclss  9760  dmttrcl  9761  rnttrcl  9762  ttrclselem2  9766  ackbij1lem15  10273  pwfseqlem4a  10701  pwfseqlem4  10702  eluzuzle  12887  xlesubadd  13305  elioc2  13450  elico2  13451  elicc2  13452  fseq1p1m1  13638  ccatswrd  14706  pfxccat3a  14776  2cshw  14851  tanadd  16203  dvds2ln  16326  prmgaplem5  17093  prmgaplem8  17096  cshwsidrepsw  17131  ressress  17293  f1ovscpbl  17571  mreexexlem4d  17690  mreexexd  17691  2oppccomf  17768  fthmon  17974  fuccocl  18012  fucidcl  18013  invfuc  18022  initoeu2lem1  18059  curf2cl  18276  yonedalem4c  18322  yonedalem3  18325  pospo  18390  latjle12  18495  latjlej1  18498  latnlej2  18504  latlem12  18511  latmlem1  18514  latledi  18522  latjass  18528  latj12  18529  latj32  18530  latj13  18531  latj31  18532  latjrot  18533  latjjdi  18536  latjjdir  18537  latdisdlem  18541  prdssgrpd  18746  prdsmndd  18783  imasmnd2  18787  imasmnd  18788  frmdmnd  18872  grpsubadd  19046  grpaddsubass  19048  grpsubsub4  19051  grppnpcan2  19052  grpnpncan  19053  grpnnncan2  19055  imasgrp2  19073  imasgrp  19074  mulgnndir  19121  mulgnn0dir  19122  mulgnnass  19127  mulgnn0ass  19128  mulgass  19129  pwsmulg  19137  issubg2  19159  qusgrp  19204  kerf1ghm  19265  galcan  19322  gacan  19323  oppgmnd  19373  pmtrprfv  19471  pmtr3ncom  19493  psgnunilem3  19514  frgp0  19778  cmn32  19818  cmn12  19820  abladdsub  19830  ablsubaddsub  19832  ablsubsub23  19842  mulgdi  19844  mulgsubdi  19847  dprdss  20049  dprdf1o  20052  dprdsn  20056  dmdprdsplit  20067  pgpfac1lem5  20099  prdsrngd  20173  imasrng  20174  srgdilem  20189  ringdilem  20246  ringrng  20282  prdsringd  20318  imasring  20327  opprrng  20345  mulgass3  20353  dvrass  20408  dvrdir  20412  subrgunit  20590  issubrg2  20592  isdomn4  20716  abvdiv  20830  lss1  20936  lsssn0  20946  islss3  20957  prdslmodd  20967  islmhm2  21037  lspsolv  21145  lbsextlem4  21163  sralmod  21194  rnglidl1  21242  ipdi  21658  ipsubdir  21660  ipsubdi  21661  ipassr  21664  ipassr2  21665  isphld  21672  ocvlss  21690  sraassab  21888  sraassaOLD  21890  psrgrpOLD  21977  psrlmod  21980  psrring  21990  psrassa  21993  mpllsslem  22020  mamudm  22399  matring  22449  matassa  22450  ofco2  22457  scmatlss  22531  ma1repveval  22577  mdetunilem1  22618  mdetunilem9  22626  monmatcollpw  22785  iinopn  22908  restopnb  23183  subbascn  23262  hausnei2  23361  nrmsep2  23364  isnrm3  23367  t1sep  23378  regsep2  23384  dnsconst  23386  dfconn2  23427  dislly  23505  tx1stc  23658  qtophmeo  23825  filss  23861  infil  23871  fsubbas  23875  filssufilg  23919  hauspwpwf1  23995  cnextcn  24075  tmdcn2  24097  psmettri  24321  isxmet2d  24337  xmettri  24361  xmetres2  24371  bldisj  24408  blss2ps  24413  blss2  24414  xmstri2  24476  mstri2  24477  xmstri  24478  mstri  24479  xmstri3  24480  mstri3  24481  msrtri  24482  comet  24526  met2ndci  24535  ngprcan  24623  ngplcan  24624  ngpsubcan  24627  nmtri2  24640  nrgdsdi  24686  nrgdsdir  24687  nlmdsdi  24702  nlmdsdir  24703  blcvx  24819  iocopnst  24970  icccvx  24981  pi1grplem  25082  pi1xfrf  25086  pi1cof  25092  clmpm1dir  25136  cmodscmulexp  25155  cvsdiv  25165  cvsdivcl  25166  cphdivcl  25216  cphsubdir  25242  cphsubdi  25243  bcthlem5  25362  rrxcph  25426  volfiniun  25582  volcn  25641  itg1val2  25719  dvconst  25952  dvlip  26032  ftc1a  26078  ulmdvlem3  26445  ang180  26857  cvxcl  27028  scvxcvx  27029  sgmmul  27245  logexprlim  27269  dchrabl  27298  nosupbnd1  27759  noinfbnd1lem5  27772  noinfbnd1  27774  ssltsep  27835  addscom  27999  addsbday  28050  addsdi  28181  mulsass  28192  motgrp  28551  iscgra1  28818  cgrane2  28821  cgrane4  28823  cgrahl1  28824  cgrahl2  28825  cgracgr  28826  cgratr  28831  cgrabtwn  28834  cgrahl  28835  dfcgra2  28838  sacgr  28839  f1otrge  28880  xmstrkgc  28900  colinearalglem1  28921  colinearalg  28925  axcgrtr  28930  axlowdimlem16  28972  axeuclidlem  28977  axcontlem4  28982  axcontlem7  28985  axcontlem12  28990  eengtrkg  29001  eengtrkge  29002  edglnl  29160  subgruhgredgd  29301  nbfusgrlevtxm2  29395  upgrwlkdvde  29757  crctcshwlkn0lem5  29834  crctcshwlkn0  29841  umgrwwlks2on  29977  rusgrnumwwlks  29994  clwlkclwwlkfo  30028  3spthd  30195  frgr2wwlkeqm  30350  dlwwlknondlwlknonf1o  30384  numclwwlk5  30407  friendship  30418  grpomuldivass  30560  ablodivdiv4  30573  dipdi  30862  dipsubdi  30868  disjdsct  32712  omndmul2  33089  archiabllem2c  33202  dvrcan5  33240  rloccring  33274  reofld  33372  eqgvscpbl  33378  qusvsval  33380  quslmod  33386  quslmhm  33387  prmidlc  33476  ssdifidl  33485  ssmxidl  33502  ply1degltlss  33617  r1plmhm  33630  drgextlsp  33644  ccfldsrarelvec  33721  constrconj  33786  constrfin  33787  constrelextdg2  33788  pstmfval  33895  qqhval2lem  33982  qqhvq  33988  esumcvg  34087  sigaclcu  34118  measdivcst  34225  measdivcstALTV  34226  carsggect  34320  tgoldbachgtd  34677  bnj970  34961  bnj910  34962  erdszelem9  35204  cvmseu  35281  elmrsubrn  35525  r1peuqusdeg1  35648  cgrid2  36004  btwncomim  36014  btwnswapid  36018  trisegint  36029  cgrxfr  36056  btwnxfr  36057  brofs2  36078  brifs2  36079  endofsegid  36086  btwnconn1lem11  36098  btwnconn2  36103  segcon2  36106  seglemin  36114  segletr  36115  btwnsegle  36118  colinbtwnle  36119  broutsideof2  36123  btwnoutside  36126  broutsideof3  36127  outsideoftr  36130  outsidele  36133  ellines  36153  linethrueu  36157  weiunpo  36466  unbdqndv2  36512  poimirlem28  37655  ftc1anc  37708  sdclem1  37750  sstotbnd2  37781  ismndo1  37880  zerdivemp1x  37954  isdrngo2  37965  iscringd  38005  lsmsat  39009  lfladdcl  39072  lflnegcl  39076  lflvscl  39078  lshpkrlem4  39114  lshpkrlem6  39116  ldualgrplem  39146  lduallmodlem  39153  latmassOLD  39230  latm12  39231  latm32  39232  latmrot  39233  latmmdiN  39235  latmmdir  39236  omlfh1N  39259  omlfh3N  39260  cvrnbtwn2  39276  cvlexchb1  39331  cvlexch3  39333  cvlexch4N  39334  cvlatexchb1  39335  cvlsupr2  39344  hlatjass  39371  hlatj12  39372  hlatj32  39373  cvrat  39424  atcvrj0  39430  cvrat2  39431  atltcvr  39437  atexchltN  39443  cvrat3  39444  cvrat4  39445  atbtwnexOLDN  39449  atbtwnex  39450  3dimlem3  39463  3dimlem3OLDN  39464  3at  39492  2atneat  39517  llncmp  39524  2at0mat0  39527  2atmat0  39528  islpln2a  39550  llncvrlpln  39560  lplncmp  39564  3atnelvolN  39588  4atlem11  39611  lplncvrlvol  39618  lvolcmp  39619  2atm2atN  39787  elpaddatriN  39805  elpadd2at2  39809  paddasslem8  39829  paddasslem17  39838  paddass  39840  padd12N  39841  paddssw1  39845  pmodlem2  39849  pmodN  39852  pmapjlln1  39857  atmod1i2  39861  pexmidlem2N  39973  pexmidlem7N  39978  pl42lem2N  39982  pl42lem3N  39983  pl42lem4N  39984  pl42N  39985  lhp2lt  40003  lhpm0atN  40031  lautlt  40093  lautcvr  40094  lautj  40095  lautm  40096  ltrneq2  40150  cdleme1b  40228  cdleme3b  40231  cdleme3c  40232  cdleme9b  40254  cdlemefs27cl  40415  cdleme42mN  40489  cdlemg4c  40614  trljco  40742  tgrpgrplem  40751  tendoplass  40785  tendodi1  40786  tendodi2  40787  erngplus2  40806  erngplus2-rN  40814  cdlemk36  40915  erngdvlem3  40992  erngdvlem3-rN  41000  dvaplusgv  41012  tendospass  41021  tendospdi1  41022  dvalveclem  41027  dialss  41048  dvhvaddass  41099  dvhopvsca  41104  dvhlveclem  41110  diblss  41172  diclss  41195  diclspsn  41196  cdlemn11pre  41212  dihmeetlem12N  41320  dihmeetlem16N  41324  dihmeetlem17N  41325  dvh4dimN  41449  lpolsatN  41490  lpolpolsatN  41491  dochpolN  41492  lclkr  41535  lclkrs  41541  lcfr  41587  lcmineqlem13  42042  aks6d1c1  42117  irrapxlem6  42838  jm2.26lem3  43013  mpaamn  43168  mendring  43200  mendlmod  43201  mendassa  43202  nnoeomeqom  43325  omabs2  43345  neicvgel1  44132  rfcnpre4  45039  fmuldfeq  45598  stoweidlem43  46058  stoweidlem52  46067  stoweidlem53  46068  stoweidlem56  46071  issmfgt  46771  issmfge  46785  iccelpart  47420  prproropf1olem1  47490  fmtnoprmfac1  47552  fmtnoprmfac2  47554  isubgr3stgrlem2  47934  isubgr3stgrlem4  47936  grlimgrtrilem1  47961  copissgrp  48084  cznrng  48177  funcringcsetcALTV2lem9  48214  funcringcsetclem9ALTV  48237  linccl  48331  lincsumscmcl  48350  ldepsprlem  48389  lincresunit3lem1  48396  itsclc0yqe  48682  topdlat  48893  catprs  48900  endmndlem  48904  idmon  48908  idepi  48909  thincmon  49082  thincepi  49083  functhinclem1  49093  grptcmon  49190  grptcepi  49191