Theorem simpr3 1192

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 487	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜃)
2	1	3ad2antr3 1186	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpr13  1255  simpr23  1258  simpr33  1261  simp1r3  1267  simp2r3  1273  simp3r3  1279  3anandis  1467  funopsn  6913  fpr2g  6977  isopolem  7101  fr3nr  7497  suppfnss  7858  elfir  8882  intrnfi  8883  fisupcl  8936  cnfcomlem  9165  ackbij1lem15  9659  pwfseqlem4a  10086  pwfseqlem4  10087  eluzuzle  12255  xlesubadd  12659  elioc2  12802  elico2  12803  elicc2  12804  fseq1p1m1  12984  ccatswrd  14033  pfxccat3a  14103  2cshw  14178  tanadd  15523  dvds2ln  15645  prmgaplem5  16394  prmgaplem8  16397  cshwsidrepsw  16430  ressress  16565  f1ovscpbl  16802  mreexexlem4d  16921  mreexexd  16922  2oppccomf  16998  fthmon  17200  fuccocl  17237  fucidcl  17238  invfuc  17247  initoeu2lem1  17277  curf2cl  17484  yonedalem4c  17530  yonedalem3  17533  pospo  17586  latjle12  17675  latjlej1  17678  latnlej2  17684  latlem12  17691  latmlem1  17694  latledi  17702  latjass  17708  latj12  17709  latj32  17710  latj13  17711  latj31  17712  latjrot  17713  latjjdi  17716  latjjdir  17717  latdisdlem  17802  prdsmndd  17947  imasmnd2  17951  imasmnd  17952  frmdmnd  18027  grpsubadd  18190  grpaddsubass  18192  grpsubsub4  18195  grppnpcan2  18196  grpnpncan  18197  grpnnncan2  18199  imasgrp2  18217  imasgrp  18218  mulgnndir  18259  mulgnn0dir  18260  mulgnnass  18265  mulgnn0ass  18266  mulgass  18267  pwsmulg  18275  issubg2  18297  qusgrp  18338  galcan  18437  gacan  18438  oppgmnd  18485  pmtrprfv  18584  pmtr3ncom  18606  psgnunilem3  18627  frgp0  18889  cmn32  18928  cmn12  18930  abladdsub  18938  ablsubsub23  18948  mulgdi  18950  mulgsubdi  18953  dprdss  19154  dprdf1o  19157  dprdsn  19161  dmdprdsplit  19172  pgpfac1lem5  19204  srgi  19264  ringi  19313  prdsringd  19365  imasring  19372  opprring  19384  mulgass3  19390  dvrass  19443  kerf1ghm  19500  kerf1hrmOLD  19501  subrgunit  19556  issubrg2  19558  abvdiv  19611  lss1  19713  lsssn0  19722  islss3  19734  prdslmodd  19744  islmhm2  19813  lspsolv  19918  lbsextlem4  19936  sralmod  19962  sraassa  20102  psrbaglesupp  20151  psrbagcon  20154  psrgrp  20181  psrlmod  20184  psrring  20194  psrassa  20197  mpllsslem  20218  ipdi  20787  ipsubdir  20789  ipsubdi  20790  ipassr  20793  ipassr2  20794  isphld  20801  ocvlss  20819  mamudm  21002  matring  21055  matassa  21056  ofco2  21063  scmatlss  21137  ma1repveval  21183  mdetunilem1  21224  mdetunilem9  21232  monmatcollpw  21390  iinopn  21513  restopnb  21786  subbascn  21865  hausnei2  21964  nrmsep2  21967  isnrm3  21970  t1sep  21981  regsep2  21987  dnsconst  21989  dfconn2  22030  dislly  22108  tx1stc  22261  qtophmeo  22428  filss  22464  infil  22474  fsubbas  22478  filssufilg  22522  hauspwpwf1  22598  cnextcn  22678  tmdcn2  22700  psmettri  22924  isxmet2d  22940  xmettri  22964  xmetres2  22974  bldisj  23011  blss2ps  23016  blss2  23017  xmstri2  23079  mstri2  23080  xmstri  23081  mstri  23082  xmstri3  23083  mstri3  23084  msrtri  23085  comet  23126  met2ndci  23135  ngprcan  23222  ngplcan  23223  ngpsubcan  23226  nmtri2  23239  nrgdsdi  23277  nrgdsdir  23278  nlmdsdi  23293  nlmdsdir  23294  blcvx  23409  iocopnst  23547  icccvx  23557  pi1grplem  23656  pi1xfrf  23660  pi1cof  23666  clmpm1dir  23710  cmodscmulexp  23729  cvsdiv  23739  cvsdivcl  23740  cphdivcl  23789  cphsubdir  23815  cphsubdi  23816  bcthlem5  23934  rrxcph  23998  volfiniun  24151  volcn  24210  itg1val2  24288  dvconst  24517  dvlip  24593  ftc1a  24637  ulmdvlem3  24993  ang180  25395  cvxcl  25565  scvxcvx  25566  sgmmul  25780  logexprlim  25804  dchrabl  25833  motgrp  26332  iscgra1  26599  cgrane2  26602  cgrane4  26604  cgrahl1  26605  cgrahl2  26606  cgracgr  26607  cgratr  26612  cgrabtwn  26615  cgrahl  26616  dfcgra2  26619  sacgr  26620  f1otrge  26661  xmstrkgc  26675  colinearalglem1  26695  colinearalg  26699  axcgrtr  26704  axlowdimlem16  26746  axeuclidlem  26751  axcontlem4  26756  axcontlem7  26759  axcontlem12  26764  eengtrkg  26775  eengtrkge  26776  edglnl  26931  subgruhgredgd  27069  nbfusgrlevtxm2  27163  upgrwlkdvde  27521  crctcshwlkn0lem5  27595  crctcshwlkn0  27602  umgrwwlks2on  27739  rusgrnumwwlks  27756  clwlkclwwlkfo  27790  3spthd  27958  frgr2wwlkeqm  28113  dlwwlknondlwlknonf1o  28147  numclwwlk5  28170  friendship  28181  grpomuldivass  28321  ablodivdiv4  28334  dipdi  28623  dipsubdi  28629  disjdsct  30441  omndmul2  30717  archiabllem2c  30828  dvrdir  30865  dvrcan5  30868  reofld  30917  eqgvscpbl  30923  qusscaval  30925  quslmod  30927  quslmhm  30928  prmidlc  30968  ssmxidl  30983  drgextlsp  31000  ccfldsrarelvec  31060  pstmfval  31140  qqhval2lem  31226  qqhvq  31232  esumcvg  31349  sigaclcu  31380  measdivcst  31487  measdivcstALTV  31488  carsggect  31580  tgoldbachgtd  31937  bnj970  32223  bnj910  32224  erdszelem9  32450  cvmseu  32527  elmrsubrn  32771  noprefixmo  33206  nosupbnd1  33218  ssltsep  33263  cgrid2  33468  btwncomim  33478  btwnswapid  33482  trisegint  33493  cgrxfr  33520  btwnxfr  33521  brofs2  33542  brifs2  33543  endofsegid  33550  btwnconn1lem11  33562  btwnconn2  33567  segcon2  33570  seglemin  33578  segletr  33579  btwnsegle  33582  colinbtwnle  33583  broutsideof2  33587  btwnoutside  33590  broutsideof3  33591  outsideoftr  33594  outsidele  33597  ellines  33617  linethrueu  33621  unbdqndv2  33854  poimirlem28  34924  ftc1anc  34979  sdclem1  35022  sstotbnd2  35056  ismndo1  35155  zerdivemp1x  35229  isdrngo2  35240  iscringd  35280  lsmsat  36148  lfladdcl  36211  lflnegcl  36215  lflvscl  36217  lshpkrlem4  36253  lshpkrlem6  36255  ldualgrplem  36285  lduallmodlem  36292  latmassOLD  36369  latm12  36370  latm32  36371  latmrot  36372  latmmdiN  36374  latmmdir  36375  omlfh1N  36398  omlfh3N  36399  cvrnbtwn2  36415  cvlexchb1  36470  cvlexch3  36472  cvlexch4N  36473  cvlatexchb1  36474  cvlsupr2  36483  hlatjass  36510  hlatj12  36511  hlatj32  36512  cvrat  36562  atcvrj0  36568  cvrat2  36569  atltcvr  36575  atexchltN  36581  cvrat3  36582  cvrat4  36583  atbtwnexOLDN  36587  atbtwnex  36588  3dimlem3  36601  3dimlem3OLDN  36602  3at  36630  2atneat  36655  llncmp  36662  2at0mat0  36665  2atmat0  36666  islpln2a  36688  llncvrlpln  36698  lplncmp  36702  3atnelvolN  36726  4atlem11  36749  lplncvrlvol  36756  lvolcmp  36757  2atm2atN  36925  elpaddatriN  36943  elpadd2at2  36947  paddasslem8  36967  paddasslem17  36976  paddass  36978  padd12N  36979  paddssw1  36983  pmodlem2  36987  pmodN  36990  pmapjlln1  36995  atmod1i2  36999  pexmidlem2N  37111  pexmidlem7N  37116  pl42lem2N  37120  pl42lem3N  37121  pl42lem4N  37122  pl42N  37123  lhp2lt  37141  lhpm0atN  37169  lautlt  37231  lautcvr  37232  lautj  37233  lautm  37234  ltrneq2  37288  cdleme1b  37366  cdleme3b  37369  cdleme3c  37370  cdleme9b  37392  cdlemefs27cl  37553  cdleme42mN  37627  cdlemg4c  37752  trljco  37880  tgrpgrplem  37889  tendoplass  37923  tendodi1  37924  tendodi2  37925  erngplus2  37944  erngplus2-rN  37952  cdlemk36  38053  erngdvlem3  38130  erngdvlem3-rN  38138  dvaplusgv  38150  tendospass  38159  tendospdi1  38160  dvalveclem  38165  dialss  38186  dvhvaddass  38237  dvhopvsca  38242  dvhlveclem  38248  diblss  38310  diclss  38333  diclspsn  38334  cdlemn11pre  38350  dihmeetlem12N  38458  dihmeetlem16N  38462  dihmeetlem17N  38463  dvh4dimN  38587  lpolsatN  38628  lpolpolsatN  38629  dochpolN  38630  lclkr  38673  lclkrs  38679  lcfr  38725  irrapxlem6  39430  jm2.26lem3  39604  mpaamn  39762  mendring  39798  mendlmod  39799  mendassa  39800  neicvgel1  40475  rfcnpre4  41297  fmuldfeq  41870  stoweidlem43  42335  stoweidlem52  42344  stoweidlem53  42345  stoweidlem56  42348  issmfgt  43040  issmfge  43053  iccelpart  43600  prproropf1olem1  43672  fmtnoprmfac1  43734  fmtnoprmfac2  43736  copissgrp  44082  ringrng  44157  cznrng  44233  funcringcsetcALTV2lem9  44322  funcringcsetclem9ALTV  44345  linccl  44476  lincsumscmcl  44495  ldepsprlem  44534  lincresunit3lem1  44541  itsclc0yqe  44755