Theorem simp33l 1301

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

Assertion

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

Proof of Theorem simp33l

Step	Hyp	Ref	Expression
1		simp3l 1202	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant3 1135	1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  totprob  34394  cdleme19b  40283  cdleme19d  40285  cdleme19e  40286  cdleme20h  40295  cdleme20l2  40300  cdleme20m  40302  cdleme21d  40309  cdleme21e  40310  cdleme22e  40323  cdleme22f2  40326  cdleme22g  40327  cdleme26e  40338  cdleme28a  40349  cdleme28b  40350  cdleme37m  40441  cdleme39n  40445  cdlemeg46gfre  40511  cdlemg28a  40672  cdlemg28b  40682  cdlemk3  40812  cdlemk5a  40814  cdlemk6  40816  cdlemkuat  40845  cdlemkid2  40903