Theorem simp33l 1319

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

Assertion

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

Proof of Theorem simp33l

Step	Hyp	Ref	Expression
1		simp3l 1220	. 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  35042  cdleme19b  41329  cdleme19d  41331  cdleme19e  41332  cdleme20h  41341  cdleme20l2  41346  cdleme20m  41348  cdleme21d  41355  cdleme21e  41356  cdleme22e  41369  cdleme22f2  41372  cdleme22g  41373  cdleme26e  41384  cdleme28a  41395  cdleme28b  41396  cdleme37m  41487  cdleme39n  41491  cdlemeg46gfre  41557  cdlemg28a  41718  cdlemg28b  41728  cdlemk3  41858  cdlemk5a  41860  cdlemk6  41862  cdlemkuat  41891  cdlemkid2  41949