Theorem simp13r 1291

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

Assertion

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

Proof of Theorem simp13r

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

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

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 1089

This theorem is referenced by:  pceu  16786  axpasch  29026  3dimlem4  39837  3atlem4  39859  llncvrlpln2  39930  2lplnja  39992  lhpmcvr5N  40400  4atexlemswapqr  40436  4atexlemnclw  40443  trlval2  40536  cdleme21h  40707  cdleme24  40725  cdleme26ee  40733  cdleme26f  40736  cdleme26f2  40738  cdlemf1  40934  cdlemg16ALTN  41031  cdlemg17iqN  41047  cdlemg27b  41069  trlcone  41101  cdlemg48  41110  tendocan  41197  cdlemk26-3  41279  cdlemk27-3  41280  cdlemk28-3  41281  cdlemk37  41287  cdlemky  41299  cdlemk11ta  41302  cdlemkid3N  41306  cdlemk11t  41319  cdlemk46  41321  cdlemk47  41322  cdlemk51  41326  cdlemk52  41327  cdleml4N  41352  dihmeetlem1N  41663  dihmeetlem20N  41699  mapdpglem32  42078  addlimc  46003  iscnrm3rlem8  49303