Theorem simprlr 792

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 490	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 741	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fcof1  7283  fliftfun  7308  fprresex  8306  domunfican  9291  finsschain  9326  suppeqfsuppbi  9349  fsuppunbi  9359  wemapsolem  9522  wemapso  9523  wemapso2lem  9524  cantnf  9672  enfin2i  10370  ttukeylem7  10564  fpwwe2lem2  10688  fpwwe2lem8  10694  fpwwe2lem11  10697  fpwwelem  10701  distrlem4pr  11082  mulcmpblnr  11127  prsrlem1  11128  addsrmo  11129  mulsrmo  11130  divdivdiv  11987  divsubdiv  12002  lediv12a  12179  xmullem  13363  xlemul1a  13387  seqcaopr  14150  leexp2r  14285  hashf1lem1  14567  hashf1lem2  14568  fi1uzind  14619  brfi1indALT  14622  wrd2ind  14839  swrdccat  14851  cshweqrep  14939  rtrclreclem4  15181  summolem2  15849  summo  15850  prodmolem2  16069  prodmo  16070  bezoutlem3  16678  bezoutlem4  16679  qredeu  16795  pcadd  17028  vdwlem9  17128  vdwlem10  17129  ramub1lem2  17166  ramub1  17167  cofucl  18024  setcmon  18223  poslubmo  18544  posglbmo  18545  grprcan  19145  isnsg3  19331  ghmpreima  19413  gaorber  19483  psgneu  19681  odcau  19779  lsmsubm  19828  lsmmod  19850  efgsfo  19914  ablfaclem3  20264  rngpropd  20357  ringpropd  20480  islmodd  21102  lmodprop2d  21160  lss1d  21199  lindff1  22087  islindf4  22105  assamulgscmlem2  22169  mplcoe1  22307  mplcoe5  22310  evlslem1  22352  mdetunilem7  22894  mdetunilem8  22895  mdetunilem9  22896  mdetuni0  22897  mdetmul  22899  ppttop  23286  epttop  23288  cnhaus  23633  isreg2  23656  cncmp  23671  1stcfb  23724  2ndcomap  23738  cldllycmp  23775  txcls  23884  ptclsg  23895  ptcnp  23902  txdis1cn  23915  txlly  23916  txnlly  23917  pthaus  23918  txhaus  23927  txkgen  23932  xkohaus  23933  xkococnlem  23939  xkococn  23940  fgabs  24159  rnelfm  24233  hausflimi  24260  hausflim  24261  alexsubALTlem2  24328  alexsubALTlem4  24330  alexsubALT  24331  tgpconncomp  24393  qustgplem  24401  metequiv2  24790  met2ndci  24802  nrmmetd  24854  nlmvscnlem1  24966  reconn  25109  xrge0tsms  25115  ipcnlem1  25527  minveclem3  25711  pmltpc  25732  ovolicc2lem5  25803  ovolicc2  25804  uniioombllem6  25870  dyadmbllem  25881  vitalilem3  25892  mbfmullem  26007  itg2split  26031  itg2mono  26035  bddiblnc  26123  dvlip2  26276  lhop1  26295  dvcnvrelem1  26298  ftc1lem6  26322  itgsubst  26330  dgrco  26555  plyexmo  26599  ulmdvlem3  26692  abelthlem2  26722  abelthlem8  26729  mpodvdsmulf1o  27484  dvdsmulf1o  27486  chpchtsum  27509  dchrptlem2  27555  2sqlem5  27712  2sqlem9  27717  2sqb  27722  pntrlog2bnd  27874  pntibndlem3  27882  pntlemp  27900  pnt3  27902  noresle  27987  nosupprefixmo  27990  noinfprefixmo  27991  addsprop  28295  mulsproplem9  28443  mulsasslem3  28484  oncutlt  28583  expadds  28754  bdayfinbndlem1  28786  readdscl  28818  tgjustf  28868  hlcgreu  29017  mirreu3  29059  cgraswap  29260  cgracom  29262  cgratr  29263  flatcgra  29265  acopyeu  29275  brprlng  29349  axsegcon  29438  ax5seglem9  29448  axeuclid  29474  axcontlem12  29486  clwwlkf1  30573  n4cyclfrgr  30825  frgrnbnb  30827  ablo4  31085  smcnlem  31232  pjhthmo  31837  pjpjpre  31954  3oalem2  32198  lnconi  32568  atom1d  32888  resf1o  33255  mgcoval  33480  xrge0tsmsd  33567  erlval  33752  ballotlemfc0  35059  ballotlemfcc  35060  pconnconn  35917  cvmfolem  35965  cvmliftmo  35970  cvmliftlem7  35977  cvmlift2lem10  35998  cvmlift3lem8  36012  lineext  36763  linecgr  36768  btwnconn1lem10  36783  btwnconn1lem11  36784  btwnconn3  36790  brsegle  36795  seglecgr12im  36797  segleantisym  36802  outsideoftr  36816  outsideofeq  36817  outsideofeu  36818  linethru  36840  nadddilem1  36891  finminlem  37028  neibastop2lem  37070  weiunpo  37175  isbasisrelowllem1  38198  isbasisrelowllem2  38199  mblfinlem3  38497  ftc1cnnc  38530  isbnd3  38638  heibor1lem  38663  crngm4  38857  cvlcvr1  40316  4atlem12  40589  paddasslem12  40808  paddasslem13  40809  lhpexle2lem  40986  trlord  41546  cdlemkid4  41911  dihopelvalcpre  42225  dihmeetlem1N  42267  dihglblem5apreN  42268  dihmeetlem6  42286  dih1dimatlem0  42305  dihjatcclem4  42398  unitscyglem4  43168  prjspner1  43576  mzpcl2  43679  mzpmfp  43696  mzpcompact2lem  43700  diophin  43721  pell14qrmulcl  43808  hbtlem2  44069  iunrelexpuztr  44663  stoweidlem61  46993  fourierdlem92  47130  euoreqb  48101  prproropf1olem3  48509  prproropf1olem4  48510  fpprwpprb  48760  cycldlenngric  48948  grimgrtri  48969  snlindsntor  49505  elfzolborelfzop1  49553  nn0sumshdiglemB  49654  2arwcat  50630