Theorem simprll 504

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 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  5012  fcof1  5454  mpt20  5605  eroveu  6263  addcmpblnq  6619  mulcmpblnq  6620  ordpipqqs  6626  addcmpblnq0  6695  mulcmpblnq0  6696  nnnq0lem1  6698  prarloclemcalc  6754  addlocpr  6788  distrlem4prl  6836  distrlem4pru  6837  ltpopr  6847  addcmpblnr  6978  mulcmpblnrlemg  6979  mulcmpblnr  6980  prsrlem1  6981  ltsrprg  6986  apreap  7754  apreim  7770  divdivdivap  7868  divmuleqap  7872  divadddivap  7882  divsubdivap  7883  ledivdiv  8035  lediv12a  8039  exbtwnz  9337  iseqcaopr  9558  leexp2r  9627  recvguniq  10019  rsqrmo  10051  qredeu  10623  pw2dvdseu  10690