Theorem simplrr 502

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  rmob  2906  isotr  5476  riota5f  5512  tfrexlem  5971  fopwdom  6333  fisbth  6367  fin0  6369  fin0or  6370  diffisn  6377  fientri3  6381  fnfi  6388  ordiso2  6446  addcmpblnq  6557  mulcmpblnq  6558  ordpipqqs  6564  ltexnqq  6598  addcmpblnq0  6633  mulcmpblnq0  6634  prmu  6668  addlocpr  6726  prmuloc  6756  prmuloc2  6757  ltaddpr  6787  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemloc  6797  ltexprlemrl  6800  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  aptiprleml  6829  aptiprlemu  6830  ltmprr  6832  cauappcvgprlemloc  6842  archrecpr  6854  caucvgprlemloc  6865  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  addcmpblnr  6916  mulcmpblnrlemg  6917  mulcmpblnr  6918  ltsrprg  6924  mulgt0sr  6954  caucvgsrlemgt1  6971  axmulcl  7034  axarch  7057  axcaucvglemres  7065  readdcan  7248  cnegexlem1  7283  negeu  7299  add20  7578  apreap  7687  cru  7702  apsym  7706  apcotr  7707  apadd1  7708  apneg  7711  mulext1  7712  divdivdivap  7801  ltmul12a  7938  lemul12a  7940  lt2mul2div  7957  ledivdiv  7968  lediv12a  7972  qapne  8724  ixxss12  8929  ioodisj  9015  fz0fzelfz0  9138  qtri3or  9252  qbtwnzlemstep  9257  qbtwnzlemex  9259  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2z  9263  qbtwnre  9265  btwnzge0  9302  expivallem  9477  mulexpzap  9516  leexp1a  9531  expnbnd  9596  cjap  9793  cvg1nlemres  9871  rsqrmo  9913  abs3lem  9997  cau3lem  10000  rexanre  10106  climcau  10184  addmodlteqALT  10259  divalglemeunn  10321  divalglemeuneg  10323  zsupcllemstep  10341  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlembi  10394  bezoutlemeu  10396  rpdvds  10481  isprm6  10526  pw2dvdslemn  10543  pw2dvdseu  10546  sqrt2irrap  10558  qdencn  10785