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  17056  axpasch  29552  3dimlem4  40724  3atlem4  40746  llncvrlpln2  40817  2lplnja  40879  lhpmcvr5N  41287  4atexlemswapqr  41323  4atexlemnclw  41330  trlval2  41423  cdleme21h  41594  cdleme24  41612  cdleme26ee  41620  cdleme26f  41623  cdleme26f2  41625  cdlemf1  41821  cdlemg16ALTN  41918  cdlemg17iqN  41934  cdlemg27b  41956  trlcone  41988  cdlemg48  41997  tendocan  42084  cdlemk26-3  42166  cdlemk27-3  42167  cdlemk28-3  42168  cdlemk37  42174  cdlemky  42186  cdlemk11ta  42189  cdlemkid3N  42193  cdlemk11t  42206  cdlemk46  42208  cdlemk47  42209  cdlemk51  42213  cdlemk52  42214  cdleml4N  42239  dihmeetlem1N  42550  dihmeetlem20N  42586  mapdpglem32  42965  addlimc  46873  iscnrm3rlem8  50276