Theorem simprrl 507

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 108	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 476	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:  dn1dc  909  imain  5130  grpridd  5879  tfrlemisucaccv  6128  tfrexlem  6137  tfr1onlemsucaccv  6144  tfrcllemsucaccv  6157  eroveu  6423  addcmpblnq  7023  mulcmpblnq  7024  ordpipqqs  7030  nqnq0pi  7094  addcmpblnq0  7099  mulcmpblnq0  7100  prarloclemcalc  7158  prarloc  7159  nqpru  7208  mullocpr  7227  distrlem4prl  7240  distrlem4pru  7241  ltprordil  7245  ltexprlemm  7256  ltexprlemopu  7259  ltexprlemupu  7260  ltexprlemru  7268  cauappcvgprlemopl  7302  cauappcvgprlem2  7316  caucvgprlemopl  7325  caucvgprlem2  7336  caucvgprprlemexbt  7362  caucvgprprlem2  7366  addcmpblnr  7382  mulcmpblnrlemg  7383  mulcmpblnr  7384  prsrlem1  7385  ltsrprg  7390  axmulcl  7500  ltmul1  8166  divdivdivap  8277  divmuleqap  8281  divsubdivap  8292  lt2mul2div  8437  ledivdiv  8448  lediv12a  8452  ssfzo12bi  9785  exbtwnz  9811  qbtwnre  9817  ioom  9821  seq3caopr  10033  leexp2r  10124  hashunlem  10327  recvguniq  10543  rsqrmo  10575  fsum2dlemstep  10977  expcnvre  11046  bezout  11427  qredeu  11506  pw2dvdseu  11573  oddpwdclemdvds  11575  neiint  11997  restbasg  12020  iscnp4  12069  cnpnei  12070  cnptopco  12073  blssps  12213  blss  12214  metequiv2  12282