Theorem simp13r 1308

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

Assertion

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

Proof of Theorem simp13r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pceu  16931  axpasch  29328  3dimlem4  40279  3atlem4  40301  llncvrlpln2  40372  2lplnja  40434  lhpmcvr5N  40842  4atexlemswapqr  40878  4atexlemnclw  40885  trlval2  40978  cdleme21h  41149  cdleme24  41167  cdleme26ee  41175  cdleme26f  41178  cdleme26f2  41180  cdlemf1  41376  cdlemg16ALTN  41473  cdlemg17iqN  41489  cdlemg27b  41511  trlcone  41543  cdlemg48  41552  tendocan  41639  cdlemk26-3  41721  cdlemk27-3  41722  cdlemk28-3  41723  cdlemk37  41729  cdlemky  41741  cdlemk11ta  41744  cdlemkid3N  41748  cdlemk11t  41761  cdlemk46  41763  cdlemk47  41764  cdlemk51  41768  cdlemk52  41769  cdleml4N  41794  dihmeetlem1N  42105  dihmeetlem20N  42141  mapdpglem32  42520  addlimc  46403  iscnrm3rlem8  49766