Theorem simplrl 487

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplrl	⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 102	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 458	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  rmob  2850  f1imass  5413  riota5f  5492  tfrexlem  5948  fopwdom  6310  fidceq  6330  fisbth  6340  fientri3  6353  ordiso2  6357  addcmpblnq  6465  mulcmpblnq  6466  ordpipqqs  6472  addcmpblnq0  6541  mulcmpblnq0  6542  prml  6575  addlocpr  6634  prmuloc  6664  mullocpr  6669  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemloc  6705  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  aptiprleml  6737  ltmprr  6740  cauappcvgprlemopl  6744  cauappcvgprlemopu  6746  cauappcvgprlemloc  6750  caucvgprlemopl  6767  caucvgprlemopu  6769  caucvgprlemloc  6773  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgprprlemaddq  6806  addcmpblnr  6824  mulcmpblnrlemg  6825  mulcmpblnr  6826  ltsrprg  6832  mulgt0sr  6862  caucvgsrlemgt1  6879  axmulcl  6942  axcaucvglemres  6973  cnegexlem1  7186  negeu  7202  add20  7469  apreap  7578  cru  7593  apsym  7597  apcotr  7598  apadd1  7599  apneg  7602  mulext1  7603  mulge0  7610  mulap0  7635  divdivdivap  7689  prodgt0  7818  ltmul12a  7826  lt2mul2div  7845  ledivdiv  7856  lediv12a  7860  qapne  8574  ixxss12  8775  elfz0ubfz0  8982  qtri3or  9098  qbtwnzlemstep  9103  qbtwnzlemex  9105  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2z  9109  btwnzge0  9142  expivallem  9256  mulexpzap  9295  leexp1a  9309  cjap  9506  cvg1nlemres  9584  rsqrmo  9625  abslt  9684  abs3lem  9707  cau3lem  9710  climcau  9866  qdencn  10124