Theorem simplrr 776

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplrr	⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Proof of Theorem simplrr

Step	Hyp	Ref	Expression
1		simpr 483	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 725	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  disjxiun  5149  frpomin  6352  fsnex  7296  f1prex  7297  isotr  7347  weniso  7365  riota5f  7408  frxp2  8157  frxp3  8164  xpord3pred  8165  poseq  8171  fprlem2  8315  tfrlem9a  8415  oaass  8590  oeeui  8631  oaabs2  8678  coflton  8700  cofon1  8701  naddssim  8714  resixpfo  8964  omxpenlem  9110  pw2f1olem  9113  fopwdom  9117  fofinf1o  9367  marypha1lem  9472  ordiso2  9554  oismo  9579  ixpiunwdom  9629  cantnf  9732  ttrclss  9759  fseqenlem1  10063  iunfictbso  10153  dfac12lem2  10183  dfac12lem3  10184  infunsdom1  10252  infpssrlem5  10346  fin23lem24  10361  isf32lem2  10393  isf32lem4  10395  isf34lem4  10416  fin1a2lem12  10450  fin1a2lem13  10451  ttukeylem6  10553  fpwwe2lem11  10680  fpwwe2lem12  10681  fpwwe2  10682  winalim2  10735  wunex2  10777  tskord  10819  prlem934  11072  mulcmpblnr  11110  dedekind  11423  addrid  11440  cnegex  11441  negeu  11496  add20  11772  divdivdiv  11962  ltmul12a  12117  lemul12a  12119  lediv12a  12154  supaddc  12228  supmul1  12230  cru  12251  uzwo3  12974  xleadd1a  13281  xmullem  13292  xmulgt0  13311  xlemul1a  13316  ixxun  13389  ixxss12  13393  ioodisj  13508  fz0fzelfz0  13656  mulexpz  14117  rpexpmord  14182  leexp1a  14189  expmulnbnd  14247  hashf1  14471  fi1uzind  14511  brfi1indALT  14514  swrdccat  14738  reuccatpfxs1  14750  abs3lem  15338  rexanre  15346  cau3lem  15354  limsupgre  15478  limsupbnd2  15480  o1lo1  15534  rlimclim1  15542  rlimclim  15543  rlimcn1  15585  rlimcn3  15587  o1of2  15610  o1rlimmul  15616  lo1add  15624  lo1mul  15625  isercolllem1  15664  climcau  15670  caucvgrlem  15672  caucvgb  15679  summolem2  15715  summo  15716  modfsummod  15793  o1fsum  15812  prodmolem2  15932  addmodlteqALT  16322  rpdvds  16656  isprm5  16703  isprm6  16710  pclem  16835  pcqmul  16850  pcexp  16856  pcneg  16871  pcprmpw2  16879  pcadd  16886  pcmpt  16889  4sqlem13  16954  vdwlem2  16979  vdwlem7  16984  vdwlem12  16989  ramval  17005  ramub2  17011  ramz2  17021  ramcl  17026  cshwshashlem2  17094  imasval  17521  imasdsval  17525  mreexexd  17656  acsfn  17667  issubc3  17863  idfucl  17895  funcres2c  17918  isnat  17965  fucpropd  17997  xpcval  18196  xpcco  18202  prfval  18218  evlf2  18238  evlfcl  18242  curf12  18247  curf1cl  18248  curf2  18249  curfcl  18252  curf2ndf  18267  hof2val  18276  hofcl  18279  hofpropd  18287  yonedalem4a  18295  yonedainv  18301  drsdirfi  18325  pospo  18365  poslubmo  18431  posglbmo  18432  isipodrs  18557  acsinfd  18576  gsumvalx  18664  gsumpropd2lem  18667  mgmhmeql  18704  sgrppropd  18719  ismndd  18744  mndpropd  18747  mhmeql  18811  mndind  18813  frmdup3lem  18851  mhmmnd  19053  issubg4  19134  ssnmz  19155  conjnmzb  19242  f1otrspeq  19440  psgneu  19499  pgpfi  19598  sylow2blem3  19615  slwhash  19617  fislw  19618  sylow3lem2  19621  lsmdisj2  19675  pj1eu  19689  efgredlem  19740  frgpuplem  19765  gexex  19846  frgpnabl  19868  dprdfadd  20015  dpjidcl  20053  pgpfac1lem3  20072  pgpfaclem3  20078  ablfac2  20084  ablsimpgcygd  20101  ablsimpgfind  20105  ablsimpgprmd  20110  rngpropd  20152  ringpropd  20262  imadrhmcl  20725  islmhm2  20963  lmhmpropd  20998  lbsextlem4  21089  prmirredlem  21454  psgndiflemA  21589  lsmcss  21680  uvcf1  21782  frlmsslsp  21786  frlmup1  21788  assapropd  21861  psrval  21904  evlslem1  22089  mamucl  22384  mamuass  22385  mamudi  22386  mamudir  22387  mamuvs1  22388  mamuvs2  22389  mamulid  22426  mamurid  22427  dmatsubcl  22483  dmatmulcl  22485  scmatscm  22498  marrepval  22547  marepveval  22553  mdetunilem7  22603  gsummatr01lem4  22643  cpmatmcllem  22703  mat2pmatf1  22714  mat2pmatlin  22720  decpmatmul  22757  pm2mpmhmlem2  22804  chpidmat  22832  pptbas  22994  toponmre  23080  restbas  23145  iscncl  23256  cnrest2  23273  cnpdis  23280  lmcnp  23291  dishaus  23369  cmpcovf  23378  tgcmp  23388  dfconn2  23406  clsconn  23417  2ndcctbss  23442  dis2ndc  23447  1stccnp  23449  islly2  23471  cldllycmp  23482  locfincmp  23513  comppfsc  23519  kgentopon  23525  txcls  23591  ptpjopn  23599  dfac14  23605  xkoccn  23606  txcnp  23607  txcmpb  23631  txlm  23635  xkopt  23642  xkoco1cn  23644  xkoco2cn  23645  qtopcn  23701  qtoprest  23704  regr1lem2  23727  xkocnv  23801  qtophmeo  23804  fmfnfmlem4  23944  hausflim  23968  hauspwpwf1  23974  fclscmp  24017  alexsublem  24031  alexsubALTlem2  24035  alexsubALTlem3  24036  ptcmplem3  24041  ptcmplem4  24042  ptcmplem5  24043  cnextfun  24051  tmdgsum2  24083  symgtgp  24093  tsmsval2  24117  tsmsgsum  24126  utoptop  24222  ismet2  24322  blin  24410  metss2lem  24503  methaus  24512  met1stc  24513  met2ndci  24514  prdsxmslem2  24521  metcnp3  24532  metcnpi3  24538  metustto  24545  metustfbas  24549  nlmvscn  24687  nrginvrcn  24692  xrsxmet  24808  reconnlem1  24825  reconn  24827  xrge0tsms  24833  xmetdcn2  24836  metdscn  24855  addcnlem  24863  fsumcn  24871  cnheiborlem  24963  cnheibor  24964  bndth  24967  lebnum  24973  nmoleub2lem2  25126  ipcn  25257  iscmet3  25304  caubl  25319  rrxdstprj1  25420  minveclem3b  25439  minveclem7  25446  pjthlem2  25449  pmltpc  25462  volfiniun  25559  ioombl1  25574  dyadss  25606  dyaddisjlem  25607  dyadmax  25610  dyadmbllem  25611  opnmbllem  25613  itg1addlem2  25709  itg10a  25723  mbfi1fseqlem6  25733  itg2seq  25755  itg2monolem1  25763  itg2gt0  25773  itgfsum  25839  limcfval  25884  ellimc2  25889  ellimc3  25891  limcres  25898  limciun  25906  dvres  25923  dveflem  25994  rolle  26005  dvlip2  26011  c1liplem1  26012  dvgt0lem1  26018  dvgt0  26020  dvlt0  26021  dvne0  26027  dvfsumrlimge0  26048  ftc1lem6  26059  itgsubst  26067  mdegmullem  26097  ply1domn  26143  ply1divex  26156  fta1g  26189  fta1b  26191  plyf  26217  dgrlem  26248  coeid  26257  plydivalg  26319  aannenlem1  26348  aalioulem3  26354  aalioulem6  26357  abelthlem8  26461  efif1olem4  26564  chordthm  26857  xrlimcnp  26988  jensen  27009  lgamcvglem  27060  lgamcvg2  27075  sqf11  27159  fsumvma2  27235  perfectlem2  27251  lgsdilem  27345  lgsquad2lem2  27406  lgsquad3  27408  2sqlem5  27443  2sqlem9  27448  2sqb  27453  rpvmasumlem  27508  dchrisum0flb  27531  dchrisum0  27541  pntpbnd  27609  pntibndlem3  27613  pntleml  27632  nolt02o  27717  nosupbday  27727  nosupbnd2  27738  noinfbday  27742  noinfbnd2  27753  noetasuplem4  27758  noetainflem4  27762  noetalem1  27763  conway  27821  slerec  27841  sltlpss  27922  addsprop  27982  remulscllem2  28344  tgjustc1  28394  tgjustc2  28395  legov  28504  legtrid  28510  tglinethru  28555  tglnpt2  28560  tglineintmo  28561  mirreu3  28573  perpcom  28632  colperpexlem3  28651  mideu  28657  opphllem1  28666  hlpasch  28675  lnopp2hpgb  28682  trgcopy  28723  brcgr  28826  brbtwn2  28831  colinearalg  28836  axsegcon  28853  axeuclidlem  28888  axcontlem9  28898  ecgrtg  28909  elntg  28910  eengtrkg  28912  upgr1eopALT  29045  usgredg4  29145  subuhgr  29214  subumgr  29216  usgr2wspthon  29891  clwlkclwwlkf1  29935  eupth2lems  30163  n4cyclfrgr  30216  vacn  30619  blocni  30730  ubthlem3  30797  minvecolem7  30808  chocunii  31226  pjhthmo  31227  pjhthlem2  31317  kbass5  32045  mdsymlem5  32332  foresf1o  32421  fcobij  32627  xrofsup  32660  mgcoval  32844  mgcf1o  32861  xrge0tsmsd  32903  symgcntz  32940  archirngz  33031  archiabllem2a  33036  isarchiofld  33172  prmidl2  33293  smatrcl  33567  reff  33610  ordtconnlem1  33695  qqhval2  33753  volmeas  34020  fiunelcarsg  34106  ballotlemfc0  34282  ballotlemfcc  34283  signstfvneq0  34374  derangenlem  34951  erdsze2lem1  34983  pconnconn  35011  connpconn  35015  cvxsconn  35023  cvmliftmolem2  35062  cvmliftmo  35064  cvmlift2lem10  35092  cvmlift2lem12  35094  cvmlift3lem7  35105  mrsubff1  35294  msubff1  35336  r1peuqusdeg1  35423  ifscgr  35816  cgrxfr  35827  btwnconn1lem13  35871  btwnconn1lem14  35872  outsideofeq  35902  ellines  35924  finminlem  35978  fnejoin2  36029  unbdqndv2  36162  irrdiff  36981  poimirlem13  37282  poimirlem14  37283  poimirlem32  37301  opnmbllem0  37305  mblfinlem3  37308  itg2addnclem  37320  itg2addnc  37323  ftc1cnnc  37341  upixp  37378  filbcmb  37389  sstotbnd2  37423  isbnd3  37433  prdsbnd2  37444  cntotbnd  37445  ismtyima  37452  bfp  37473  rrncmslem  37481  unichnidl  37680  lshpcmp  38634  islshpat  38663  lfl0f  38715  ishlat3N  39000  3dim1  39114  islvol5  39226  lvoli2  39228  lncvrelatN  39428  pclfinclN  39597  pexmidlem8N  39624  idltrn  39797  cdleme42keg  40133  cdleme42mgN  40135  cdlemf2  40209  cdlemg2cex  40238  trlcoat  40370  dihopelvalcpre  40895  dih1dimatlem  40976  dihjatcclem4  41068  lcfl7N  41148  lcfrlem9  41197  mapdh9a  41436  hdmapglem7  41576  aks4d1p8  41734  isprimroot  41740  evl1gprodd  41763  sticksstones11  41802  imacrhmcl  41935  fsuppind  42004  fsuppssind  42007  mhpind  42008  renegeulemv  42090  sn-subeu  42148  remulinvcom  42154  sn-itrere  42188  sn-retire  42189  prjspertr  42196  prjspreln0  42200  flt4lem7  42250  nna4b4nsq  42251  nacsfix  42306  mzpsubst  42342  mzpcompact2lem  42345  eldioph2lem2  42355  eldioph2  42356  eldioph2b  42357  diophin  42366  diophun  42367  irrapxlem3  42418  irrapxlem5  42420  pell1234qrreccl  42448  pell1234qrmulcl  42449  pell14qrdich  42463  pell1qrge1  42464  pell1qrgaplem  42467  monotuz  42536  acongtr  42573  acongrep  42575  jm2.23  42591  jm2.26a  42595  jm2.26lem3  42596  jm2.26  42597  jm2.27  42603  wepwsolem  42640  fnwe2lem2  42649  kelac1  42661  kercvrlsm  42681  hbtlem5  42726  hbt  42728  mpaaeu  42748  cantnfresb  42927  onmcl  42934  tfsconcatun  42940  tfsconcatfn  42941  tfsconcatfv1  42942  tfsconcatfv2  42943  naddcnff  42965  rfovcnvf1od  43608  mnurndlem1  43892  cncmpmax  44568  rfcnnnub  44572  disjxp1  44607  iccintsng  45078  fprodcn  45158  lptioo2  45189  lptioo1  45190  limclner  45209  stoweidlem31  45589  stoweidlem34  45592  stoweidlem35  45593  stoweidlem49  45607  stoweidlem59  45617  stoweidlem62  45620  fourierdlem60  45724  fourierdlem61  45725  fourierdlem87  45751  iundjiun  46018  ismeannd  46025  hoidmvle  46158  smfsuplem2  46370  2reu8i  46663  prproropf1olem2  47013  paireqne  47020  perfectALTVlem2  47231  mogoldbb  47294  bgoldbtbndlem2  47315  bgoldbtbndlem3  47316  uspgrimprop  47389  mndpsuppss  47687  scmsuppss  47688  lindslinindsimp2lem5  47782  elfzolborelfzop1  47839  elbigolo1  47882  itschlc0xyqsol1  48091  itschlc0xyqsol  48092  iccdisj  48169  toslat  48245  functhinclem4  48302