Theorem simprll 489

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 102	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrl 459	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:  imain  4981  fcof1  5423  mpt20  5574  eroveu  6197  addcmpblnq  6465  mulcmpblnq  6466  ordpipqqs  6472  addcmpblnq0  6541  mulcmpblnq0  6542  nnnq0lem1  6544  prarloclemcalc  6600  addlocpr  6634  distrlem4prl  6682  distrlem4pru  6683  ltpopr  6693  addcmpblnr  6824  mulcmpblnrlemg  6825  mulcmpblnr  6826  prsrlem1  6827  ltsrprg  6832  apreap  7578  apreim  7594  divdivdivap  7689  divmuleqap  7693  divadddivap  7703  divsubdivap  7704  ledivdiv  7856  lediv12a  7860  qbtwnz  9106  iseqcaopr  9242  leexp2r  9308  recvguniq  9593  rsqrmo  9625