Theorem simp13r 1290

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp13r	⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓)

Proof of Theorem simp13r

Step	Hyp	Ref	Expression
1		simp3r 1203	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1133	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  pceu  16824  axpasch  28875  3dimlem4  39465  3atlem4  39487  llncvrlpln2  39558  2lplnja  39620  lhpmcvr5N  40028  4atexlemswapqr  40064  4atexlemnclw  40071  trlval2  40164  cdleme21h  40335  cdleme24  40353  cdleme26ee  40361  cdleme26f  40364  cdleme26f2  40366  cdlemf1  40562  cdlemg16ALTN  40659  cdlemg17iqN  40675  cdlemg27b  40697  trlcone  40729  cdlemg48  40738  tendocan  40825  cdlemk26-3  40907  cdlemk27-3  40908  cdlemk28-3  40909  cdlemk37  40915  cdlemky  40927  cdlemk11ta  40930  cdlemkid3N  40934  cdlemk11t  40947  cdlemk46  40949  cdlemk47  40950  cdlemk51  40954  cdlemk52  40955  cdleml4N  40980  dihmeetlem1N  41291  dihmeetlem20N  41327  mapdpglem32  41706  addlimc  45653  iscnrm3rlem8  48939