Theorem simpr3 1195

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simpr13  1258  simpr23  1261  simpr33  1264  simp1r3  1270  simp2r3  1276  simp3r3  1282  3anandis  1470  funopsn  7013  fpr2g  7080  isopolem  7209  fr3nr  7613  suppfnss  7993  elfir  9162  intrnfi  9163  fisupcl  9216  cnfcomlem  9445  ttrclss  9466  dmttrcl  9467  rnttrcl  9468  ttrclselem2  9472  ackbij1lem15  9978  pwfseqlem4a  10405  pwfseqlem4  10406  eluzuzle  12579  xlesubadd  12985  elioc2  13130  elico2  13131  elicc2  13132  fseq1p1m1  13318  ccatswrd  14369  pfxccat3a  14439  2cshw  14514  tanadd  15864  dvds2ln  15986  prmgaplem5  16744  prmgaplem8  16747  cshwsidrepsw  16783  ressress  16946  f1ovscpbl  17225  mreexexlem4d  17344  mreexexd  17345  2oppccomf  17424  fthmon  17631  fuccocl  17670  fucidcl  17671  invfuc  17680  initoeu2lem1  17717  curf2cl  17937  yonedalem4c  17983  yonedalem3  17986  pospo  18051  latjle12  18156  latjlej1  18159  latnlej2  18165  latlem12  18172  latmlem1  18175  latledi  18183  latjass  18189  latj12  18190  latj32  18191  latj13  18192  latj31  18193  latjrot  18194  latjjdi  18197  latjjdir  18198  latdisdlem  18202  prdsmndd  18406  imasmnd2  18410  imasmnd  18411  frmdmnd  18486  grpsubadd  18651  grpaddsubass  18653  grpsubsub4  18656  grppnpcan2  18657  grpnpncan  18658  grpnnncan2  18660  imasgrp2  18678  imasgrp  18679  mulgnndir  18720  mulgnn0dir  18721  mulgnnass  18726  mulgnn0ass  18727  mulgass  18728  pwsmulg  18736  issubg2  18758  qusgrp  18799  galcan  18898  gacan  18899  oppgmnd  18949  pmtrprfv  19049  pmtr3ncom  19071  psgnunilem3  19092  frgp0  19354  cmn32  19393  cmn12  19395  abladdsub  19404  ablsubsub23  19414  mulgdi  19416  mulgsubdi  19419  dprdss  19620  dprdf1o  19623  dprdsn  19627  dmdprdsplit  19638  pgpfac1lem5  19670  srgi  19735  ringi  19787  prdsringd  19839  imasring  19846  opprring  19861  mulgass3  19867  dvrass  19920  kerf1ghm  19975  subrgunit  20030  issubrg2  20032  abvdiv  20085  lss1  20188  lsssn0  20197  islss3  20209  prdslmodd  20219  islmhm2  20288  lspsolv  20393  lbsextlem4  20411  sralmod  20445  ipdi  20833  ipsubdir  20835  ipsubdi  20836  ipassr  20839  ipassr2  20840  isphld  20847  ocvlss  20865  sraassa  21062  psrbaglesuppOLD  21116  psrbagconOLD  21122  psrgrp  21155  psrlmod  21158  psrring  21168  psrassa  21171  mpllsslem  21194  mamudm  21525  matring  21580  matassa  21581  ofco2  21588  scmatlss  21662  ma1repveval  21708  mdetunilem1  21749  mdetunilem9  21757  monmatcollpw  21916  iinopn  22039  restopnb  22314  subbascn  22393  hausnei2  22492  nrmsep2  22495  isnrm3  22498  t1sep  22509  regsep2  22515  dnsconst  22517  dfconn2  22558  dislly  22636  tx1stc  22789  qtophmeo  22956  filss  22992  infil  23002  fsubbas  23006  filssufilg  23050  hauspwpwf1  23126  cnextcn  23206  tmdcn2  23228  psmettri  23452  isxmet2d  23468  xmettri  23492  xmetres2  23502  bldisj  23539  blss2ps  23544  blss2  23545  xmstri2  23607  mstri2  23608  xmstri  23609  mstri  23610  xmstri3  23611  mstri3  23612  msrtri  23613  comet  23657  met2ndci  23666  ngprcan  23754  ngplcan  23755  ngpsubcan  23758  nmtri2  23771  nrgdsdi  23817  nrgdsdir  23818  nlmdsdi  23833  nlmdsdir  23834  blcvx  23949  iocopnst  24091  icccvx  24101  pi1grplem  24200  pi1xfrf  24204  pi1cof  24210  clmpm1dir  24254  cmodscmulexp  24273  cvsdiv  24283  cvsdivcl  24284  cphdivcl  24334  cphsubdir  24360  cphsubdi  24361  bcthlem5  24480  rrxcph  24544  volfiniun  24699  volcn  24758  itg1val2  24836  dvconst  25069  dvlip  25145  ftc1a  25189  ulmdvlem3  25549  ang180  25952  cvxcl  26122  scvxcvx  26123  sgmmul  26337  logexprlim  26361  dchrabl  26390  motgrp  26892  iscgra1  27159  cgrane2  27162  cgrane4  27164  cgrahl1  27165  cgrahl2  27166  cgracgr  27167  cgratr  27172  cgrabtwn  27175  cgrahl  27176  dfcgra2  27179  sacgr  27180  f1otrge  27221  xmstrkgc  27241  colinearalglem1  27262  colinearalg  27266  axcgrtr  27271  axlowdimlem16  27313  axeuclidlem  27318  axcontlem4  27323  axcontlem7  27326  axcontlem12  27331  eengtrkg  27342  eengtrkge  27343  edglnl  27501  subgruhgredgd  27639  nbfusgrlevtxm2  27733  upgrwlkdvde  28091  crctcshwlkn0lem5  28165  crctcshwlkn0  28172  umgrwwlks2on  28308  rusgrnumwwlks  28325  clwlkclwwlkfo  28359  3spthd  28526  frgr2wwlkeqm  28681  dlwwlknondlwlknonf1o  28715  numclwwlk5  28738  friendship  28749  grpomuldivass  28889  ablodivdiv4  28902  dipdi  29191  dipsubdi  29197  disjdsct  31021  omndmul2  31324  archiabllem2c  31435  dvrdir  31473  dvrcan5  31476  reofld  31530  eqgvscpbl  31536  qusscaval  31538  quslmod  31540  quslmhm  31541  prmidlc  31610  ssmxidl  31628  drgextlsp  31667  ccfldsrarelvec  31727  pstmfval  31832  qqhval2lem  31917  qqhvq  31923  esumcvg  32040  sigaclcu  32071  measdivcst  32178  measdivcstALTV  32179  carsggect  32271  tgoldbachgtd  32628  bnj970  32913  bnj910  32914  erdszelem9  33147  cvmseu  33224  elmrsubrn  33468  xpord3pred  33784  sexp3  33785  nosupbnd1  33903  noinfbnd1lem5  33916  noinfbnd1  33918  ssltsep  33971  addscom  34115  cgrid2  34291  btwncomim  34301  btwnswapid  34305  trisegint  34316  cgrxfr  34343  btwnxfr  34344  brofs2  34365  brifs2  34366  endofsegid  34373  btwnconn1lem11  34385  btwnconn2  34390  segcon2  34393  seglemin  34401  segletr  34402  btwnsegle  34405  colinbtwnle  34406  broutsideof2  34410  btwnoutside  34413  broutsideof3  34414  outsideoftr  34417  outsidele  34420  ellines  34440  linethrueu  34444  unbdqndv2  34677  poimirlem28  35791  ftc1anc  35844  sdclem1  35887  sstotbnd2  35918  ismndo1  36017  zerdivemp1x  36091  isdrngo2  36102  iscringd  36142  lsmsat  37008  lfladdcl  37071  lflnegcl  37075  lflvscl  37077  lshpkrlem4  37113  lshpkrlem6  37115  ldualgrplem  37145  lduallmodlem  37152  latmassOLD  37229  latm12  37230  latm32  37231  latmrot  37232  latmmdiN  37234  latmmdir  37235  omlfh1N  37258  omlfh3N  37259  cvrnbtwn2  37275  cvlexchb1  37330  cvlexch3  37332  cvlexch4N  37333  cvlatexchb1  37334  cvlsupr2  37343  hlatjass  37370  hlatj12  37371  hlatj32  37372  cvrat  37422  atcvrj0  37428  cvrat2  37429  atltcvr  37435  atexchltN  37441  cvrat3  37442  cvrat4  37443  atbtwnexOLDN  37447  atbtwnex  37448  3dimlem3  37461  3dimlem3OLDN  37462  3at  37490  2atneat  37515  llncmp  37522  2at0mat0  37525  2atmat0  37526  islpln2a  37548  llncvrlpln  37558  lplncmp  37562  3atnelvolN  37586  4atlem11  37609  lplncvrlvol  37616  lvolcmp  37617  2atm2atN  37785  elpaddatriN  37803  elpadd2at2  37807  paddasslem8  37827  paddasslem17  37836  paddass  37838  padd12N  37839  paddssw1  37843  pmodlem2  37847  pmodN  37850  pmapjlln1  37855  atmod1i2  37859  pexmidlem2N  37971  pexmidlem7N  37976  pl42lem2N  37980  pl42lem3N  37981  pl42lem4N  37982  pl42N  37983  lhp2lt  38001  lhpm0atN  38029  lautlt  38091  lautcvr  38092  lautj  38093  lautm  38094  ltrneq2  38148  cdleme1b  38226  cdleme3b  38229  cdleme3c  38230  cdleme9b  38252  cdlemefs27cl  38413  cdleme42mN  38487  cdlemg4c  38612  trljco  38740  tgrpgrplem  38749  tendoplass  38783  tendodi1  38784  tendodi2  38785  erngplus2  38804  erngplus2-rN  38812  cdlemk36  38913  erngdvlem3  38990  erngdvlem3-rN  38998  dvaplusgv  39010  tendospass  39019  tendospdi1  39020  dvalveclem  39025  dialss  39046  dvhvaddass  39097  dvhopvsca  39102  dvhlveclem  39108  diblss  39170  diclss  39193  diclspsn  39194  cdlemn11pre  39210  dihmeetlem12N  39318  dihmeetlem16N  39322  dihmeetlem17N  39323  dvh4dimN  39447  lpolsatN  39488  lpolpolsatN  39489  dochpolN  39490  lclkr  39533  lclkrs  39539  lcfr  39585  lcmineqlem13  40035  isdomn4  40158  irrapxlem6  40635  jm2.26lem3  40809  mpaamn  40967  mendring  41003  mendlmod  41004  mendassa  41005  neicvgel1  41688  rfcnpre4  42536  fmuldfeq  43083  stoweidlem43  43543  stoweidlem52  43552  stoweidlem53  43553  stoweidlem56  43556  issmfgt  44248  issmfge  44261  iccelpart  44841  prproropf1olem1  44911  fmtnoprmfac1  44973  fmtnoprmfac2  44975  copissgrp  45318  ringrng  45393  cznrng  45469  funcringcsetcALTV2lem9  45558  funcringcsetclem9ALTV  45581  linccl  45711  lincsumscmcl  45730  ldepsprlem  45769  lincresunit3lem1  45776  itsclc0yqe  46063  topdlat  46246  catprs  46248  endmndlem  46252  idmon  46253  idepi  46254  thincmon  46271  thincepi  46272  functhinclem1  46278  grptcmon  46333  grptcepi  46334