Theorem simp33r 1320

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

Assertion

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

Proof of Theorem simp33r

Step	Hyp	Ref	Expression
1		simp3r 1221	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant3 1153	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:  totprob  35142  cdleme19b  41564  cdleme19e  41567  cdleme20h  41576  cdleme20l2  41581  cdleme20m  41583  cdleme21d  41590  cdleme21e  41591  cdleme22eALTN  41605  cdleme22f2  41607  cdleme22g  41608  cdleme26e  41619  cdleme37m  41722  cdlemeg46gfre  41792  cdlemg28a  41953  cdlemg28b  41963  cdlemk5a  42095  cdlemk6  42097