Theorem simprlr 506

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

Assertion

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

Proof of Theorem simprlr

Step	Hyp	Ref	Expression
1		simpr 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 475	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  imain  5130  fcof1  5600  fliftfun  5613  sbthlemi6  6751  sbthlemi8  6753  addcmpblnq  7023  mulcmpblnq  7024  ordpipqqs  7030  enq0tr  7090  addcmpblnq0  7099  mulcmpblnq0  7100  nnnq0lem1  7102  addnq0mo  7103  mulnq0mo  7104  prarloclemcalc  7158  addlocpr  7192  distrlem4prl  7240  distrlem4pru  7241  addcmpblnr  7382  mulcmpblnrlemg  7383  mulcmpblnr  7384  prsrlem1  7385  addsrmo  7386  mulsrmo  7387  ltsrprg  7390  apreap  8161  apreim  8177  divdivdivap  8277  divsubdivap  8292  ledivdiv  8448  lediv12a  8452  exbtwnz  9811  seq3caopr  10049  leexp2r  10140  zfz1iso  10377  recvguniq  10559  rsqrmo  10591  summodclem2  10940  qredeu  11521  pw2dvdseu  11588  epttop  11957  metequiv2  12297