Theorem simprrl 529

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 483	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  dn1dc  950  imain  5269  grpridd  6034  tfrlemisucaccv  6289  tfrexlem  6298  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  eroveu  6588  addcmpblnq  7304  mulcmpblnq  7305  ordpipqqs  7311  nqnq0pi  7375  addcmpblnq0  7380  mulcmpblnq0  7381  prarloclemcalc  7439  prarloc  7440  nqpru  7489  mullocpr  7508  distrlem4prl  7521  distrlem4pru  7522  ltprordil  7526  ltexprlemm  7537  ltexprlemopu  7540  ltexprlemupu  7541  ltexprlemru  7549  cauappcvgprlemopl  7583  cauappcvgprlem2  7597  caucvgprlemopl  7606  caucvgprlem2  7617  caucvgprprlemexbt  7643  caucvgprprlem2  7647  suplocexprlemloc  7658  suplocexprlemub  7660  suplocexprlemlub  7661  addcmpblnr  7676  mulcmpblnrlemg  7677  mulcmpblnr  7678  prsrlem1  7679  ltsrprg  7684  axmulcl  7803  ltmul1  8486  divdivdivap  8605  divmuleqap  8609  divsubdivap  8620  lt2mul2div  8770  ledivdiv  8781  lediv12a  8785  ssfzo12bi  10156  exbtwnz  10182  qbtwnre  10188  ioom  10192  seq3caopr  10414  leexp2r  10505  hashunlem  10713  recvguniq  10933  rsqrmo  10965  fsum2dlemstep  11371  expcnvre  11440  fprod2dlemstep  11559  suprzcl2dc  11884  bezout  11940  qredeu  12025  pw2dvdseu  12096  oddpwdclemdvds  12098  pcqmul  12231  pcadd  12267  pockthg  12283  neiint  12745  restbasg  12768  iscnp4  12818  cnpnei  12819  cnptopco  12822  blssps  13027  blss  13028  metequiv2  13096  xmetxpbl  13108  suplociccex  13203  dedekindicc  13211  limcimolemlt  13233  2sqlem5  13555