Theorem simprrl 539

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 109	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 491	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  dn1dc  960  imain  5295  tfrlemisucaccv  6321  tfrexlem  6330  tfr1onlemsucaccv  6337  tfrcllemsucaccv  6350  eroveu  6621  addcmpblnq  7361  mulcmpblnq  7362  ordpipqqs  7368  nqnq0pi  7432  addcmpblnq0  7437  mulcmpblnq0  7438  prarloclemcalc  7496  prarloc  7497  nqpru  7546  mullocpr  7565  distrlem4prl  7578  distrlem4pru  7579  ltprordil  7583  ltexprlemm  7594  ltexprlemopu  7597  ltexprlemupu  7598  ltexprlemru  7606  cauappcvgprlemopl  7640  cauappcvgprlem2  7654  caucvgprlemopl  7663  caucvgprlem2  7674  caucvgprprlemexbt  7700  caucvgprprlem2  7704  suplocexprlemloc  7715  suplocexprlemub  7717  suplocexprlemlub  7718  addcmpblnr  7733  mulcmpblnrlemg  7734  mulcmpblnr  7735  prsrlem1  7736  ltsrprg  7741  axmulcl  7860  ltmul1  8543  divdivdivap  8664  divmuleqap  8668  divsubdivap  8679  lt2mul2div  8830  ledivdiv  8841  lediv12a  8845  ssfzo12bi  10218  exbtwnz  10244  qbtwnre  10250  ioom  10254  seq3caopr  10476  leexp2r  10567  hashunlem  10775  recvguniq  10995  rsqrmo  11027  fsum2dlemstep  11433  expcnvre  11502  fprod2dlemstep  11621  suprzcl2dc  11946  bezout  12002  qredeu  12087  pw2dvdseu  12158  oddpwdclemdvds  12160  pcqmul  12293  pcadd  12329  pockthg  12345  grpridd  12736  issubmd  12793  unitgrp  13184  neiint  13427  restbasg  13450  iscnp4  13500  cnpnei  13501  cnptopco  13504  blssps  13709  blss  13710  metequiv2  13778  xmetxpbl  13790  suplociccex  13885  dedekindicc  13893  limcimolemlt  13915  2sqlem5  14237