Theorem simplrr 536

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  3123  disjiun  4081  isotr  5952  riota5f  5993  tfrexlem  6495  tfrcl  6525  nnsucuniel  6658  pw2f1odclem  7015  fopwdom  7017  dif1enen  7064  fisbth  7067  fin0  7069  fin0or  7070  diffisn  7077  fidcen  7083  finexdc  7087  elssdc  7089  fientri3  7102  unfidisj  7109  undifdc  7111  ssfirab  7123  fnfi  7129  iunfidisj  7139  dcfi  7174  ordiso2  7228  difinfinf  7294  ctmlemr  7301  exmidfodomrlemr  7406  2omotaplemap  7469  cc2lem  7478  cc3  7480  addcmpblnq  7580  mulcmpblnq  7581  ordpipqqs  7587  ltexnqq  7621  addcmpblnq0  7656  mulcmpblnq0  7657  prmu  7691  addlocpr  7749  prmuloc  7779  prmuloc2  7780  ltaddpr  7810  ltexprlemopl  7814  ltexprlemopu  7816  ltexprlemloc  7820  ltexprlemrl  7823  ltexprlemru  7825  addcanprleml  7827  addcanprlemu  7828  aptiprleml  7852  aptiprlemu  7853  ltmprr  7855  cauappcvgprlemloc  7865  archrecpr  7877  caucvgprlemloc  7888  caucvgprprlemloc  7916  caucvgprprlemexbt  7919  suplocexprlemdisj  7933  suplocexprlemloc  7934  addcmpblnr  7952  mulcmpblnrlemg  7953  mulcmpblnr  7954  ltsrprg  7960  mulgt0sr  7991  caucvgsrlemgt1  8008  suplocsrlemb  8019  axmulcl  8079  axarch  8104  axcaucvglemres  8112  axpre-suploclemres  8114  axpre-suploc  8115  readdcan  8312  cnegexlem1  8347  negeu  8363  add20  8647  apreap  8760  cru  8775  apsym  8779  apcotr  8780  apadd1  8781  apneg  8784  mulext1  8785  divdivdivap  8886  ltmul12a  9033  lemul12a  9035  lt2mul2div  9052  ledivdiv  9063  lediv12a  9067  qapne  9866  xleadd1a  10101  ixxss12  10134  ioodisj  10221  fz0fzelfz0  10355  zsupcllemstep  10482  zsupssdc  10491  qtri3or  10493  exbtwnzlemstep  10500  exbtwnzlemex  10502  exbtwnz  10503  rebtwn2zlemstep  10505  rebtwn2z  10507  qbtwnre  10509  btwnzge0  10553  iseqf1olemqf1o  10761  mulexpzap  10834  leexp1a  10849  expnbnd  10918  hashen  11039  fihashdom  11059  hashun  11061  zfz1iso  11098  swrdccat  11309  reuccatpfxs1  11321  cjap  11460  cvg1nlemres  11539  rsqrmo  11581  abs3lem  11665  cau3lem  11668  rexanre  11774  xrmaxltsup  11812  climcau  11901  sumeq2  11913  summodc  11937  fsum3cvg3  11950  fsum2d  11989  prodeq2  12111  prodmodclem2  12131  fprod2d  12177  eirrap  12332  addmodlteqALT  12413  divalglemeunn  12475  divalglemeuneg  12477  bezoutlemnewy  12560  bezoutlemstep  12561  bezoutlemmain  12562  bezoutlembi  12569  bezoutlemeu  12571  rpdvds  12664  isprm5lem  12706  isprm6  12712  pw2dvdslemn  12730  pw2dvdseu  12733  sqrt2irrap  12745  pythagtriplem2  12832  pythagtrip  12849  pclemub  12853  pcqmul  12869  pcexp  12875  pcneg  12891  pcprmpw2  12899  pcadd  12906  pcmpt  12909  4sqlem13m  12969  ennnfonelemrnh  13030  ennnfonelemnn0  13036  ctinfomlemom  13041  ctiunctlemfo  13053  nninfdclemf1  13066  imasival  13382  gsumpropd2  13469  sgrppropd  13489  ismndd  13513  mndpropd  13516  mhmeql  13568  mhmmnd  13696  issubg4m  13773  ssnmz  13791  conjnmzb  13860  rngpropd  13961  ringpropd  14044  islmod  14298  psrval  14673  restbasg  14885  cnrest2  14953  cnpdis  14959  lmtopcnp  14967  txcnp  14988  txlm  14996  ismet2  15071  blininf  15141  metss2lem  15214  xmettxlem  15226  xmettx  15227  metcnp3  15228  metcnpi3  15234  addcncntoplem  15278  fsumcncntop  15284  mulcncf  15325  dedekindeulemuub  15334  dedekindeu  15340  dedekindicclemuub  15343  ivthinclemlopn  15353  ivthinclemuopn  15355  ivthinclemloc  15358  ivthinc  15360  ivthdichlem  15368  limcimo  15382  limccnp2cntop  15394  plyf  15454  plyco  15476  plycj  15478  plyrecj  15480  dvply2g  15483  logbgcd1irrap  15687  perfectlem2  15717  lgsdilem  15749  lgsquad2lem2  15804  lgsquad3  15806  2sqlem5  15841  2sqlem9  15846  usgredg4  16059  usgr1vr  16092  clwwlknonex2lem2  16247  2omap  16544  qdencn  16581  apdiff  16602  gfsumval  16630