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  966  imain  5406  tfrlemisucaccv  6482  tfrexlem  6491  tfr1onlemsucaccv  6498  tfrcllemsucaccv  6511  eroveu  6786  addcmpblnq  7570  mulcmpblnq  7571  ordpipqqs  7577  nqnq0pi  7641  addcmpblnq0  7646  mulcmpblnq0  7647  prarloclemcalc  7705  prarloc  7706  nqpru  7755  mullocpr  7774  distrlem4prl  7787  distrlem4pru  7788  ltprordil  7792  ltexprlemm  7803  ltexprlemopu  7806  ltexprlemupu  7807  ltexprlemru  7815  cauappcvgprlemopl  7849  cauappcvgprlem2  7863  caucvgprlemopl  7872  caucvgprlem2  7883  caucvgprprlemexbt  7909  caucvgprprlem2  7913  suplocexprlemloc  7924  suplocexprlemub  7926  suplocexprlemlub  7927  addcmpblnr  7942  mulcmpblnrlemg  7943  mulcmpblnr  7944  prsrlem1  7945  ltsrprg  7950  axmulcl  8069  ltmul1  8755  divdivdivap  8876  divmuleqap  8880  divsubdivap  8891  lt2mul2div  9042  ledivdiv  9053  lediv12a  9057  ssfzo12bi  10448  suprzcl2dc  10476  exbtwnz  10487  qbtwnre  10493  ioom  10497  seq3caopr  10734  seqcaoprg  10735  leexp2r  10832  hashunlem  11043  wrd2ind  11276  recvguniq  11527  rsqrmo  11559  fsum2dlemstep  11966  expcnvre  12035  fprod2dlemstep  12154  bezout  12553  qredeu  12640  pw2dvdseu  12711  oddpwdclemdvds  12713  pcqmul  12847  pcadd  12884  pockthg  12901  grprida  13441  issubmd  13528  ghmpreima  13824  unitgrp  14101  lmodprop2d  14333  lsspropdg  14416  neiint  14840  restbasg  14863  iscnp4  14913  cnpnei  14914  cnptopco  14917  blssps  15122  blss  15123  metequiv2  15191  xmetxpbl  15203  suplociccex  15320  dedekindicc  15328  limcimolemlt  15359  lgsquad2lem2  15782  2sqlem5  15819