Theorem simprlr 779

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  fcof1  7021  fliftfun  7044  wfrlem17  7954  domunfican  8775  finsschain  8815  suppeqfsuppbi  8831  fsuppunbi  8838  wemapsolem  8998  wemapso  8999  wemapso2lem  9000  cantnf  9140  enfin2i  9732  ttukeylem7  9926  fpwwe2lem2  10043  fpwwe2lem9  10049  fpwwe2lem12  10052  fpwwelem  10056  distrlem4pr  10437  mulcmpblnr  10482  prsrlem1  10483  addsrmo  10484  mulsrmo  10485  divdivdiv  11330  divsubdiv  11345  lediv12a  11522  xmullem  12645  xlemul1a  12669  seqcaopr  13403  leexp2r  13534  hashf1lem1  13809  hashf1lem2  13810  fi1uzind  13851  brfi1indALT  13854  wrd2ind  14076  swrdccat  14088  cshweqrep  14174  rtrclreclem4  14412  summolem2  15065  summo  15066  prodmolem2  15281  prodmo  15282  bezoutlem3  15879  bezoutlem4  15880  qredeu  15992  pcadd  16215  vdwlem9  16315  vdwlem10  16316  ramub1lem2  16353  ramub1  16354  cofucl  17150  setcmon  17339  poslubmo  17748  posglbmo  17749  grprcan  18129  isnsg3  18304  ghmpreima  18372  gaorber  18430  psgneu  18626  odcau  18721  lsmsubm  18770  lsmmod  18793  efgsfo  18857  ablfaclem3  19202  ringpropd  19328  islmodd  19633  lmodprop2d  19689  lss1d  19728  lindff1  20509  islindf4  20527  assamulgscmlem2  20586  mplcoe1  20705  mplcoe5  20708  evlslem1  20754  mdetunilem7  21223  mdetunilem8  21224  mdetunilem9  21225  mdetuni0  21226  mdetmul  21228  ppttop  21612  epttop  21614  cnhaus  21959  isreg2  21982  cncmp  21997  1stcfb  22050  2ndcomap  22063  cldllycmp  22100  txcls  22209  ptclsg  22220  ptcnp  22227  txdis1cn  22240  txlly  22241  txnlly  22242  pthaus  22243  txhaus  22252  txkgen  22257  xkohaus  22258  xkococnlem  22264  xkococn  22265  fgabs  22484  rnelfm  22558  hausflimi  22585  hausflim  22586  alexsubALTlem2  22653  alexsubALTlem4  22655  alexsubALT  22656  tgpconncomp  22718  qustgplem  22726  metequiv2  23117  met2ndci  23129  nrmmetd  23181  nlmvscnlem1  23292  reconn  23433  xrge0tsms  23439  ipcnlem1  23849  minveclem3  24033  pmltpc  24054  ovolicc2lem5  24125  ovolicc2  24126  uniioombllem6  24192  dyadmbllem  24203  vitalilem3  24214  mbfmullem  24329  itg2split  24353  itg2mono  24357  bddiblnc  24445  dvlip2  24598  lhop1  24617  dvcnvrelem1  24620  ftc1lem6  24644  itgsubst  24652  dgrco  24872  plyexmo  24909  ulmdvlem3  24997  abelthlem2  25027  abelthlem8  25034  dvdsmulf1o  25779  chpchtsum  25803  dchrptlem2  25849  2sqlem5  26006  2sqlem9  26011  2sqb  26016  pntrlog2bnd  26168  pntibndlem3  26176  pntlemp  26194  pnt3  26196  tgjustf  26267  hlcgreu  26412  mirreu3  26448  cgraswap  26614  cgracom  26616  cgratr  26617  flatcgra  26618  acopyeu  26628  axsegcon  26721  ax5seglem9  26731  axeuclid  26757  axcontlem12  26769  clwwlkf1  27834  n4cyclfrgr  28076  frgrnbnb  28078  ablo4  28333  smcnlem  28480  pjhthmo  29085  pjpjpre  29202  3oalem2  29446  lnconi  29816  atom1d  30136  resf1o  30492  mgcoval  30694  xrge0tsmsd  30742  ballotlemfc0  31860  ballotlemfcc  31861  pconnconn  32591  cvmfolem  32639  cvmliftmo  32644  cvmliftlem7  32651  cvmlift2lem10  32672  cvmlift3lem8  32686  noresle  33313  lineext  33650  linecgr  33655  btwnconn1lem10  33670  btwnconn1lem11  33671  btwnconn3  33677  brsegle  33682  seglecgr12im  33684  segleantisym  33689  outsideoftr  33703  outsideofeq  33704  outsideofeu  33705  linethru  33727  finminlem  33779  neibastop2lem  33821  isbasisrelowllem1  34772  isbasisrelowllem2  34773  mblfinlem3  35096  ftc1cnnc  35129  isbnd3  35222  heibor1lem  35247  crngm4  35441  cvlcvr1  36635  4atlem12  36908  paddasslem12  37127  paddasslem13  37128  lhpexle2lem  37305  trlord  37865  cdlemkid4  38230  dihopelvalcpre  38544  dihmeetlem1N  38586  dihglblem5apreN  38587  dihmeetlem6  38605  dih1dimatlem0  38624  dihjatcclem4  38717  mzpcl2  39671  mzpmfp  39688  mzpcompact2lem  39692  diophin  39713  pell14qrmulcl  39804  hbtlem2  40068  iunrelexpuztr  40420  stoweidlem61  42703  fourierdlem92  42840  euoreqb  43665  prproropf1olem3  44022  prproropf1olem4  44023  fpprwpprb  44258  snlindsntor  44880  elfzolborelfzop1  44928  nn0sumshdiglemB  45034