Theorem simprll 503

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

Assertion

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

Proof of Theorem simprll

Step	Hyp	Ref	Expression
1		simpl 107	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrl 473	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  5001  fcof1  5443  mpt20  5594  eroveu  6220  addcmpblnq  6557  mulcmpblnq  6558  ordpipqqs  6564  addcmpblnq0  6633  mulcmpblnq0  6634  nnnq0lem1  6636  prarloclemcalc  6692  addlocpr  6726  distrlem4prl  6774  distrlem4pru  6775  ltpopr  6785  addcmpblnr  6916  mulcmpblnrlemg  6917  mulcmpblnr  6918  prsrlem1  6919  ltsrprg  6924  apreap  7687  apreim  7703  divdivdivap  7801  divmuleqap  7805  divadddivap  7815  divsubdivap  7816  ledivdiv  7968  lediv12a  7972  qbtwnz  9260  iseqcaopr  9462  leexp2r  9530  recvguniq  9881  rsqrmo  9913  qredeu  10479  pw2dvdseu  10546