Theorem simprll 505

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 108	. 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  mpt20  5756  eroveu  6423  sbthlemi6  6751  sbthlemi8  6753  addcmpblnq  7023  mulcmpblnq  7024  ordpipqqs  7030  addcmpblnq0  7099  mulcmpblnq0  7100  nnnq0lem1  7102  prarloclemcalc  7158  addlocpr  7192  distrlem4prl  7240  distrlem4pru  7241  ltpopr  7251  addcmpblnr  7382  mulcmpblnrlemg  7383  mulcmpblnr  7384  prsrlem1  7385  ltsrprg  7390  apreap  8161  apreim  8177  divdivdivap  8277  divmuleqap  8281  divadddivap  8291  divsubdivap  8292  ledivdiv  8448  lediv12a  8452  exbtwnz  9811  seq3caopr  10033  leexp2r  10124  zfz1iso  10361  recvguniq  10543  rsqrmo  10575  summodclem2  10925  qredeu  11506  pw2dvdseu  11573  epttop  11942  metequiv2  12282  mulc1cncf  12344  cncfmptc  12348  cncfmptid  12349  addccncf  12351  negcncf  12353