Theorem simprrl 491

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

Assertion

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

Proof of Theorem simprrl

Step	Hyp	Ref	Expression
1		simpl 102	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 460	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:  dn1dc  867  imain  4981  grpridd  5697  tfrlemisucaccv  5939  tfrexlem  5948  eroveu  6197  addcmpblnq  6465  mulcmpblnq  6466  ordpipqqs  6472  nqnq0pi  6536  addcmpblnq0  6541  mulcmpblnq0  6542  prarloclemcalc  6600  prarloc  6601  nqpru  6650  mullocpr  6669  distrlem4prl  6682  distrlem4pru  6683  ltprordil  6687  ltexprlemm  6698  ltexprlemopu  6701  ltexprlemupu  6702  ltexprlemru  6710  cauappcvgprlemopl  6744  cauappcvgprlem2  6758  caucvgprlemopl  6767  caucvgprlem2  6778  caucvgprprlemexbt  6804  caucvgprprlem2  6808  addcmpblnr  6824  mulcmpblnrlemg  6825  mulcmpblnr  6826  prsrlem1  6827  ltsrprg  6832  axmulcl  6942  ltmul1  7583  divdivdivap  7689  divmuleqap  7693  divsubdivap  7704  lt2mul2div  7845  ledivdiv  7856  lediv12a  7860  ssfzo12bi  9081  qbtwnz  9106  qbtwnre  9111  iseqcaopr  9242  leexp2r  9308  recvguniq  9593  rsqrmo  9625