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  34849  cdleme19b  41119  cdleme19d  41121  cdleme19e  41122  cdleme20h  41131  cdleme20l2  41136  cdleme20m  41138  cdleme21d  41145  cdleme21e  41146  cdleme22e  41159  cdleme22f2  41162  cdleme22g  41163  cdleme26e  41174  cdleme28a  41185  cdleme28b  41186  cdleme37m  41277  cdleme39n  41281  cdlemeg46gfre  41347  cdlemg28a  41508  cdlemg28b  41518  cdlemk3  41648  cdlemk5a  41650  cdlemk6  41652  cdlemkuat  41681  cdlemkid2  41739