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  35105  cdleme19b  41454  cdleme19d  41456  cdleme19e  41457  cdleme20h  41466  cdleme20l2  41471  cdleme20m  41473  cdleme21d  41480  cdleme21e  41481  cdleme22e  41494  cdleme22f2  41497  cdleme22g  41498  cdleme26e  41509  cdleme28a  41520  cdleme28b  41521  cdleme37m  41612  cdleme39n  41616  cdlemeg46gfre  41682  cdlemg28a  41843  cdlemg28b  41853  cdlemk3  41983  cdlemk5a  41985  cdlemk6  41987  cdlemkuat  42016  cdlemkid2  42074