Theorem simprlr 505

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 108	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrl 474	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:  imain  5032  fcof1  5475  fliftfun  5488  addcmpblnq  6689  mulcmpblnq  6690  ordpipqqs  6696  enq0tr  6756  addcmpblnq0  6765  mulcmpblnq0  6766  nnnq0lem1  6768  addnq0mo  6769  mulnq0mo  6770  prarloclemcalc  6824  addlocpr  6858  distrlem4prl  6906  distrlem4pru  6907  addcmpblnr  7048  mulcmpblnrlemg  7049  mulcmpblnr  7050  prsrlem1  7051  addsrmo  7052  mulsrmo  7053  ltsrprg  7056  apreap  7824  apreim  7840  divdivdivap  7938  divsubdivap  7953  ledivdiv  8105  lediv12a  8109  exbtwnz  9407  iseqcaopr  9628  leexp2r  9697  recvguniq  10100  rsqrmo  10132  qredeu  10704  pw2dvdseu  10771