Theorem simprlr 778

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

Assertion

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

Proof of Theorem simprlr

Step	Hyp	Ref	Expression
1		simpr 487	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 726	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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

This theorem is referenced by:  fcof1  7042  fliftfun  7064  wfrlem17  7970  domunfican  8790  finsschain  8830  suppeqfsuppbi  8846  fsuppunbi  8853  wemapsolem  9013  wemapso  9014  wemapso2lem  9015  cantnf  9155  enfin2i  9742  ttukeylem7  9936  fpwwe2lem2  10053  fpwwe2lem9  10059  fpwwe2lem12  10062  fpwwelem  10066  distrlem4pr  10447  mulcmpblnr  10492  prsrlem1  10493  addsrmo  10494  mulsrmo  10495  divdivdiv  11340  divsubdiv  11355  lediv12a  11532  xmullem  12656  xlemul1a  12680  seqcaopr  13406  leexp2r  13537  hashf1lem1  13812  hashf1lem2  13813  fi1uzind  13854  brfi1indALT  13857  wrd2ind  14084  swrdccat  14096  cshweqrep  14182  summolem2  15072  summo  15073  prodmolem2  15288  prodmo  15289  bezoutlem3  15888  bezoutlem4  15889  qredeu  16001  pcadd  16224  vdwlem9  16324  vdwlem10  16325  ramub1lem2  16362  ramub1  16363  cofucl  17157  setcmon  17346  poslubmo  17755  posglbmo  17756  grprcan  18136  isnsg3  18311  ghmpreima  18379  gaorber  18437  psgneu  18633  odcau  18728  lsmsubm  18777  lsmmod  18800  efgsfo  18864  ablfaclem3  19208  ringpropd  19331  islmodd  19639  lmodprop2d  19695  lss1d  19734  assamulgscmlem2  20128  mplcoe1  20245  mplcoe5  20248  evlslem1  20294  lindff1  20963  islindf4  20981  mdetunilem7  21226  mdetunilem8  21227  mdetunilem9  21228  mdetuni0  21229  mdetmul  21231  ppttop  21614  epttop  21616  cnhaus  21961  isreg2  21984  cncmp  21999  1stcfb  22052  2ndcomap  22065  cldllycmp  22102  txcls  22211  ptclsg  22222  ptcnp  22229  txdis1cn  22242  txlly  22243  txnlly  22244  pthaus  22245  txhaus  22254  txkgen  22259  xkohaus  22260  xkococnlem  22266  xkococn  22267  fgabs  22486  rnelfm  22560  hausflimi  22587  hausflim  22588  alexsubALTlem2  22655  alexsubALTlem4  22657  alexsubALT  22658  tgpconncomp  22720  qustgplem  22728  metequiv2  23119  met2ndci  23131  nrmmetd  23183  nlmvscnlem1  23294  reconn  23435  xrge0tsms  23441  ipcnlem1  23847  minveclem3  24031  pmltpc  24050  ovolicc2lem5  24121  ovolicc2  24122  uniioombllem6  24188  dyadmbllem  24199  vitalilem3  24210  mbfmullem  24325  itg2split  24349  itg2mono  24353  dvlip2  24591  lhop1  24610  dvcnvrelem1  24613  ftc1lem6  24637  itgsubst  24645  dgrco  24864  plyexmo  24901  ulmdvlem3  24989  abelthlem2  25019  abelthlem8  25026  dvdsmulf1o  25770  chpchtsum  25794  dchrptlem2  25840  2sqlem5  25997  2sqlem9  26002  2sqb  26007  pntrlog2bnd  26159  pntibndlem3  26167  pntlemp  26185  pnt3  26187  tgjustf  26258  hlcgreu  26403  mirreu3  26439  cgraswap  26605  cgracom  26607  cgratr  26608  flatcgra  26609  acopyeu  26619  axsegcon  26712  ax5seglem9  26722  axeuclid  26748  axcontlem12  26760  clwwlkf1  27827  n4cyclfrgr  28069  frgrnbnb  28071  ablo4  28326  smcnlem  28473  pjhthmo  29078  pjpjpre  29195  3oalem2  29439  lnconi  29809  atom1d  30129  resf1o  30465  xrge0tsmsd  30692  ballotlemfc0  31750  ballotlemfcc  31751  pconnconn  32478  cvmfolem  32526  cvmliftmo  32531  cvmliftlem7  32538  cvmlift2lem10  32559  cvmlift3lem8  32573  noresle  33200  lineext  33537  linecgr  33542  btwnconn1lem10  33557  btwnconn1lem11  33558  btwnconn3  33564  brsegle  33569  seglecgr12im  33571  segleantisym  33576  outsideoftr  33590  outsideofeq  33591  outsideofeu  33592  linethru  33614  finminlem  33666  neibastop2lem  33708  isbasisrelowllem1  34635  isbasisrelowllem2  34636  mblfinlem3  34930  bddiblnc  34961  ftc1cnnc  34965  isbnd3  35061  heibor1lem  35086  crngm4  35280  cvlcvr1  36474  4atlem12  36747  paddasslem12  36966  paddasslem13  36967  lhpexle2lem  37144  trlord  37704  cdlemkid4  38069  dihopelvalcpre  38383  dihmeetlem1N  38425  dihglblem5apreN  38426  dihmeetlem6  38444  dih1dimatlem0  38463  dihjatcclem4  38556  mzpcl2  39325  mzpmfp  39342  mzpcompact2lem  39346  diophin  39367  pell14qrmulcl  39458  hbtlem2  39722  iunrelexpuztr  40062  stoweidlem61  42345  fourierdlem92  42482  euoreqb  43307  prproropf1olem3  43666  prproropf1olem4  43667  fpprwpprb  43904  snlindsntor  44525  elfzolborelfzop1  44573  nn0sumshdiglemB  44679