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  3053  disjiun  3993  isotr  5807  riota5f  5845  tfrexlem  6325  tfrcl  6355  nnsucuniel  6486  fopwdom  6826  dif1enen  6870  fisbth  6873  fin0  6875  fin0or  6876  diffisn  6883  finexdc  6892  fientri3  6904  unfidisj  6911  undifdc  6913  ssfirab  6923  fnfi  6926  iunfidisj  6935  dcfi  6970  ordiso2  7024  difinfinf  7090  ctmlemr  7097  exmidfodomrlemr  7191  cc2lem  7240  cc3  7242  addcmpblnq  7341  mulcmpblnq  7342  ordpipqqs  7348  ltexnqq  7382  addcmpblnq0  7417  mulcmpblnq0  7418  prmu  7452  addlocpr  7510  prmuloc  7540  prmuloc2  7541  ltaddpr  7571  ltexprlemopl  7575  ltexprlemopu  7577  ltexprlemloc  7581  ltexprlemrl  7584  ltexprlemru  7586  addcanprleml  7588  addcanprlemu  7589  aptiprleml  7613  aptiprlemu  7614  ltmprr  7616  cauappcvgprlemloc  7626  archrecpr  7638  caucvgprlemloc  7649  caucvgprprlemloc  7677  caucvgprprlemexbt  7680  suplocexprlemdisj  7694  suplocexprlemloc  7695  addcmpblnr  7713  mulcmpblnrlemg  7714  mulcmpblnr  7715  ltsrprg  7721  mulgt0sr  7752  caucvgsrlemgt1  7769  suplocsrlemb  7780  axmulcl  7840  axarch  7865  axcaucvglemres  7873  axpre-suploclemres  7875  axpre-suploc  7876  readdcan  8071  cnegexlem1  8106  negeu  8122  add20  8405  apreap  8518  cru  8533  apsym  8537  apcotr  8538  apadd1  8539  apneg  8542  mulext1  8543  divdivdivap  8643  ltmul12a  8790  lemul12a  8792  lt2mul2div  8809  ledivdiv  8820  lediv12a  8824  qapne  9612  xleadd1a  9844  ixxss12  9877  ioodisj  9964  fz0fzelfz0  10097  qtri3or  10213  exbtwnzlemstep  10218  exbtwnzlemex  10220  exbtwnz  10221  rebtwn2zlemstep  10223  rebtwn2z  10225  qbtwnre  10227  btwnzge0  10270  iseqf1olemqf1o  10463  mulexpzap  10530  leexp1a  10545  expnbnd  10613  hashen  10732  fihashdom  10751  hashun  10753  zfz1iso  10789  cjap  10883  cvg1nlemres  10962  rsqrmo  11004  abs3lem  11088  cau3lem  11091  rexanre  11197  xrmaxltsup  11234  climcau  11323  sumeq2  11335  summodc  11359  fsum3cvg3  11372  fsum2d  11411  prodeq2  11533  prodmodclem2  11553  fprod2d  11599  eirrap  11753  addmodlteqALT  11832  divalglemeunn  11893  divalglemeuneg  11895  zsupcllemstep  11913  zsupssdc  11922  bezoutlemnewy  11964  bezoutlemstep  11965  bezoutlemmain  11966  bezoutlembi  11973  bezoutlemeu  11975  rpdvds  12066  isprm5lem  12108  isprm6  12114  pw2dvdslemn  12132  pw2dvdseu  12135  sqrt2irrap  12147  pythagtriplem2  12233  pythagtrip  12250  pclemub  12254  pcqmul  12270  pcexp  12276  pcneg  12291  pcprmpw2  12299  pcadd  12306  pcmpt  12308  ennnfonelemrnh  12384  ennnfonelemnn0  12390  ctinfomlemom  12395  ctiunctlemfo  12407  nninfdclemf1  12420  ismndd  12704  mndpropd  12707  mhmeql  12738  mhmmnd  12841  ringpropd  13013  restbasg  13239  cnrest2  13307  cnpdis  13313  lmtopcnp  13321  txcnp  13342  txlm  13350  ismet2  13425  blininf  13495  metss2lem  13568  xmettxlem  13580  xmettx  13581  metcnp3  13582  metcnpi3  13588  addcncntoplem  13622  fsumcncntop  13627  mulcncf  13662  dedekindeulemuub  13666  dedekindeu  13672  dedekindicclemuub  13675  ivthinclemlopn  13685  ivthinclemuopn  13687  ivthinclemloc  13690  ivthinc  13692  limcimo  13705  limccnp2cntop  13717  logbgcd1irrap  13959  lgsdilem  13999  2sqlem5  14026  2sqlem9  14031  qdencn  14336  apdiff  14357