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  945  imain  5213  grpridd  5975  tfrlemisucaccv  6230  tfrexlem  6239  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  eroveu  6528  addcmpblnq  7199  mulcmpblnq  7200  ordpipqqs  7206  nqnq0pi  7270  addcmpblnq0  7275  mulcmpblnq0  7276  prarloclemcalc  7334  prarloc  7335  nqpru  7384  mullocpr  7403  distrlem4prl  7416  distrlem4pru  7417  ltprordil  7421  ltexprlemm  7432  ltexprlemopu  7435  ltexprlemupu  7436  ltexprlemru  7444  cauappcvgprlemopl  7478  cauappcvgprlem2  7492  caucvgprlemopl  7501  caucvgprlem2  7512  caucvgprprlemexbt  7538  caucvgprprlem2  7542  suplocexprlemloc  7553  suplocexprlemub  7555  suplocexprlemlub  7556  addcmpblnr  7571  mulcmpblnrlemg  7572  mulcmpblnr  7573  prsrlem1  7574  ltsrprg  7579  axmulcl  7698  ltmul1  8378  divdivdivap  8497  divmuleqap  8501  divsubdivap  8512  lt2mul2div  8661  ledivdiv  8672  lediv12a  8676  ssfzo12bi  10033  exbtwnz  10059  qbtwnre  10065  ioom  10069  seq3caopr  10287  leexp2r  10378  hashunlem  10582  recvguniq  10799  rsqrmo  10831  fsum2dlemstep  11235  expcnvre  11304  bezout  11735  qredeu  11814  pw2dvdseu  11882  oddpwdclemdvds  11884  neiint  12353  restbasg  12376  iscnp4  12426  cnpnei  12427  cnptopco  12430  blssps  12635  blss  12636  metequiv2  12704  xmetxpbl  12716  suplociccex  12811  dedekindicc  12819  limcimolemlt  12841