Theorem simprrl 505

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 107	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 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:  dn1dc  901  imain  5001  grpridd  5717  tfrlemisucaccv  5962  tfrexlem  5971  eroveu  6220  addcmpblnq  6557  mulcmpblnq  6558  ordpipqqs  6564  nqnq0pi  6628  addcmpblnq0  6633  mulcmpblnq0  6634  prarloclemcalc  6692  prarloc  6693  nqpru  6742  mullocpr  6761  distrlem4prl  6774  distrlem4pru  6775  ltprordil  6779  ltexprlemm  6790  ltexprlemopu  6793  ltexprlemupu  6794  ltexprlemru  6802  cauappcvgprlemopl  6836  cauappcvgprlem2  6850  caucvgprlemopl  6859  caucvgprlem2  6870  caucvgprprlemexbt  6896  caucvgprprlem2  6900  addcmpblnr  6916  mulcmpblnrlemg  6917  mulcmpblnr  6918  prsrlem1  6919  ltsrprg  6924  axmulcl  7034  ltmul1  7692  divdivdivap  7801  divmuleqap  7805  divsubdivap  7816  lt2mul2div  7957  ledivdiv  7968  lediv12a  7972  ssfzo12bi  9234  qbtwnz  9260  qbtwnre  9265  ioom  9269  iseqcaopr  9462  leexp2r  9530  recvguniq  9881  rsqrmo  9913  bezout  10400  qredeu  10479  pw2dvdseu  10546  oddpwdclemdvds  10548