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  34946  cdleme19b  41185  cdleme19d  41187  cdleme19e  41188  cdleme20h  41197  cdleme20l2  41202  cdleme20m  41204  cdleme21d  41211  cdleme21e  41212  cdleme22e  41225  cdleme22f2  41228  cdleme22g  41229  cdleme26e  41240  cdleme28a  41251  cdleme28b  41252  cdleme37m  41343  cdleme39n  41347  cdlemeg46gfre  41413  cdlemg28a  41574  cdlemg28b  41584  cdlemk3  41714  cdlemk5a  41716  cdlemk6  41718  cdlemkuat  41747  cdlemkid2  41805