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  35129  cdleme19b  41553  cdleme19d  41555  cdleme19e  41556  cdleme20h  41565  cdleme20l2  41570  cdleme20m  41572  cdleme21d  41579  cdleme21e  41580  cdleme22e  41593  cdleme22f2  41596  cdleme22g  41597  cdleme26e  41608  cdleme28a  41619  cdleme28b  41620  cdleme37m  41711  cdleme39n  41715  cdlemeg46gfre  41781  cdlemg28a  41942  cdlemg28b  41952  cdlemk3  42082  cdlemk5a  42084  cdlemk6  42086  cdlemkuat  42115  cdlemkid2  42173