Theorem simplrr 538

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 110	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 489	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  rmob  3124  disjiun  4084  isotr  5962  riota5f  6003  tfrexlem  6505  tfrcl  6535  nnsucuniel  6668  pw2f1odclem  7025  fopwdom  7027  dif1enen  7074  fisbth  7077  fin0  7079  fin0or  7080  diffisn  7087  fidcen  7093  finexdc  7097  elssdc  7099  fientri3  7112  unfidisj  7119  undifdc  7121  ssfirab  7134  fnfi  7140  iunfidisj  7150  dcfi  7185  ordiso2  7239  difinfinf  7305  ctmlemr  7312  exmidfodomrlemr  7418  2omotaplemap  7481  cc2lem  7490  cc3  7492  addcmpblnq  7592  mulcmpblnq  7593  ordpipqqs  7599  ltexnqq  7633  addcmpblnq0  7668  mulcmpblnq0  7669  prmu  7703  addlocpr  7761  prmuloc  7791  prmuloc2  7792  ltaddpr  7822  ltexprlemopl  7826  ltexprlemopu  7828  ltexprlemloc  7832  ltexprlemrl  7835  ltexprlemru  7837  addcanprleml  7839  addcanprlemu  7840  aptiprleml  7864  aptiprlemu  7865  ltmprr  7867  cauappcvgprlemloc  7877  archrecpr  7889  caucvgprlemloc  7900  caucvgprprlemloc  7928  caucvgprprlemexbt  7931  suplocexprlemdisj  7945  suplocexprlemloc  7946  addcmpblnr  7964  mulcmpblnrlemg  7965  mulcmpblnr  7966  ltsrprg  7972  mulgt0sr  8003  caucvgsrlemgt1  8020  suplocsrlemb  8031  axmulcl  8091  axarch  8116  axcaucvglemres  8124  axpre-suploclemres  8126  axpre-suploc  8127  readdcan  8324  cnegexlem1  8359  negeu  8375  add20  8659  apreap  8772  cru  8787  apsym  8791  apcotr  8792  apadd1  8793  apneg  8796  mulext1  8797  divdivdivap  8898  ltmul12a  9045  lemul12a  9047  lt2mul2div  9064  ledivdiv  9075  lediv12a  9079  qapne  9878  xleadd1a  10113  ixxss12  10146  ioodisj  10233  fz0fzelfz0  10367  zsupcllemstep  10495  zsupssdc  10504  qtri3or  10506  exbtwnzlemstep  10513  exbtwnzlemex  10515  exbtwnz  10516  rebtwn2zlemstep  10518  rebtwn2z  10520  qbtwnre  10522  btwnzge0  10566  iseqf1olemqf1o  10774  mulexpzap  10847  leexp1a  10862  expnbnd  10931  hashen  11052  fihashdom  11072  hashun  11074  zfz1iso  11111  swrdccat  11325  reuccatpfxs1  11337  cjap  11489  cvg1nlemres  11568  rsqrmo  11610  abs3lem  11694  cau3lem  11697  rexanre  11803  xrmaxltsup  11841  climcau  11930  sumeq2  11942  summodc  11967  fsum3cvg3  11980  fsum2d  12019  prodeq2  12141  prodmodclem2  12161  fprod2d  12207  eirrap  12362  addmodlteqALT  12443  divalglemeunn  12505  divalglemeuneg  12507  bezoutlemnewy  12590  bezoutlemstep  12591  bezoutlemmain  12592  bezoutlembi  12599  bezoutlemeu  12601  rpdvds  12694  isprm5lem  12736  isprm6  12742  pw2dvdslemn  12760  pw2dvdseu  12763  sqrt2irrap  12775  pythagtriplem2  12862  pythagtrip  12879  pclemub  12883  pcqmul  12899  pcexp  12905  pcneg  12921  pcprmpw2  12929  pcadd  12936  pcmpt  12939  4sqlem13m  12999  ennnfonelemrnh  13060  ennnfonelemnn0  13066  ctinfomlemom  13071  ctiunctlemfo  13083  nninfdclemf1  13096  imasival  13412  gsumpropd2  13499  sgrppropd  13519  ismndd  13543  mndpropd  13546  mhmeql  13598  mhmmnd  13726  issubg4m  13803  ssnmz  13821  conjnmzb  13890  rngpropd  13992  ringpropd  14075  islmod  14329  psrval  14704  restbasg  14921  cnrest2  14989  cnpdis  14995  lmtopcnp  15003  txcnp  15024  txlm  15032  ismet2  15107  blininf  15177  metss2lem  15250  xmettxlem  15262  xmettx  15263  metcnp3  15264  metcnpi3  15270  addcncntoplem  15314  fsumcncntop  15320  mulcncf  15361  dedekindeulemuub  15370  dedekindeu  15376  dedekindicclemuub  15379  ivthinclemlopn  15389  ivthinclemuopn  15391  ivthinclemloc  15394  ivthinc  15396  ivthdichlem  15404  limcimo  15418  limccnp2cntop  15430  plyf  15490  plyco  15512  plycj  15514  plyrecj  15516  dvply2g  15519  logbgcd1irrap  15723  perfectlem2  15753  lgsdilem  15785  lgsquad2lem2  15840  lgsquad3  15842  2sqlem5  15877  2sqlem9  15882  usgredg4  16095  usgr1vr  16128  subuhgr  16152  subumgr  16154  clwwlknonex2lem2  16318  eupth2lemsfi  16358  depindlem3  16388  2omap  16654  qdencn  16694  apdiff  16719  qdiff  16720  gfsumval  16748