Theorem simpllr 486

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simpllr	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simpllr

Step	Hyp	Ref	Expression
1		simpr 103	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	ad2antrr 457	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  f1o2ndf1  5849  tfrlem1  5923  fopwdom  6310  phplem4dom  6324  phpm  6327  phplem4on  6329  fidifsnen  6331  diffisn  6350  diffifi  6351  addcmpblnq  6465  mulcmpblnq  6466  ordpipqqs  6472  ltexnqq  6506  enq0tr  6532  addcmpblnq0  6541  mulcmpblnq0  6542  nnnq0lem1  6544  prssnqu  6578  prarloclemup  6593  nqprl  6649  nqpru  6650  mullocpr  6669  cauappcvgprlemladdfu  6752  cauappcvgprlemladdrl  6755  caucvgprlemm  6766  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlemlim  6779  caucvgprprlemml  6792  caucvgprprlemloc  6801  caucvgprprlemlim  6809  addcmpblnr  6824  mulcmpblnrlemg  6825  mulcmpblnr  6826  ltsrprg  6832  srpospr  6867  caucvgsrlemoffres  6884  axcaucvglemcau  6972  cnegexlem3  7188  negeu  7202  add20  7469  rimul  7576  apreap  7578  cru  7593  apreim  7594  apsym  7597  apcotr  7598  apadd1  7599  apneg  7602  mulext1  7603  apti  7613  mulap0  7635  prodgt0  7818  ltmul12a  7826  ledivdiv  7856  lediv12a  7860  qapne  8574  ixxss12  8775  ioodisj  8861  fznlem  8905  qtri3or  9098  qbtwnzlemstep  9103  rebtwn2zlemstep  9107  mulexpzap  9295  leexp1a  9309  expnbnd  9372  cjap  9506  caucvgre  9580  cvg1nlemres  9584  resqrexlemglsq  9620  resqrexlemga  9621  sqrtsq  9642  ltabs  9683  abs3lem  9707  cau3lem  9710  climcau  9866  climrecvg1n  9867