Theorem simprrl 528

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 482	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  944  imain  5200  grpridd  5960  tfrlemisucaccv  6215  tfrexlem  6224  tfr1onlemsucaccv  6231  tfrcllemsucaccv  6244  eroveu  6513  addcmpblnq  7168  mulcmpblnq  7169  ordpipqqs  7175  nqnq0pi  7239  addcmpblnq0  7244  mulcmpblnq0  7245  prarloclemcalc  7303  prarloc  7304  nqpru  7353  mullocpr  7372  distrlem4prl  7385  distrlem4pru  7386  ltprordil  7390  ltexprlemm  7401  ltexprlemopu  7404  ltexprlemupu  7405  ltexprlemru  7413  cauappcvgprlemopl  7447  cauappcvgprlem2  7461  caucvgprlemopl  7470  caucvgprlem2  7481  caucvgprprlemexbt  7507  caucvgprprlem2  7511  suplocexprlemloc  7522  suplocexprlemub  7524  suplocexprlemlub  7525  addcmpblnr  7540  mulcmpblnrlemg  7541  mulcmpblnr  7542  prsrlem1  7543  ltsrprg  7548  axmulcl  7667  ltmul1  8347  divdivdivap  8466  divmuleqap  8470  divsubdivap  8481  lt2mul2div  8630  ledivdiv  8641  lediv12a  8645  ssfzo12bi  9995  exbtwnz  10021  qbtwnre  10027  ioom  10031  seq3caopr  10249  leexp2r  10340  hashunlem  10543  recvguniq  10760  rsqrmo  10792  fsum2dlemstep  11196  expcnvre  11265  bezout  11688  qredeu  11767  pw2dvdseu  11835  oddpwdclemdvds  11837  neiint  12303  restbasg  12326  iscnp4  12376  cnpnei  12377  cnptopco  12380  blssps  12585  blss  12586  metequiv2  12654  xmetxpbl  12666  suplociccex  12761  dedekindicc  12769  limcimolemlt  12791