Theorem simprrr 507

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

Assertion

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

Proof of Theorem simprrr

Step	Hyp	Ref	Expression
1		simpr 108	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 475	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:  fliftfun  5536  grpridd  5798  tfrlemisucaccv  6044  tfr1onlemsucaccv  6060  tfrcllemsucaccv  6073  addcmpblnq  6870  mulcmpblnq  6871  ordpipqqs  6877  nqnq0pi  6941  addcmpblnq0  6946  mulcmpblnq0  6947  addnq0mo  6950  mulnq0mo  6951  prarloclemcalc  7005  prarloc  7006  nqprl  7054  mullocpr  7074  distrlem4prl  7087  distrlem4pru  7088  ltprordil  7092  ltexprlemlol  7105  ltexprlemopu  7106  ltexprlemupu  7107  ltexprlemru  7115  cauappcvgprlemopl  7149  cauappcvgprlem2  7163  caucvgprlemopl  7172  caucvgprlem2  7183  caucvgprprlemexbt  7209  caucvgprprlem2  7213  addcmpblnr  7229  mulcmpblnrlemg  7230  mulcmpblnr  7231  prsrlem1  7232  addsrmo  7233  mulsrmo  7234  ltsrprg  7237  axmulcl  7347  recriota  7369  ltmul1  8010  divdivdivap  8119  divsubdivap  8134  ledivdiv  8286  lediv12a  8290  exbtwnz  9590  qbtwnre  9596  ioom  9600  iseqcaopr  9817  leexp2r  9908  hashunlem  10109  recvguniq  10324  rsqrmo  10356  bezout  10882  qredeu  10961  pw2dvdseu  11028  oddpwdclemndvds  11031