Theorem simp33l 1307

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

Assertion

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

Proof of Theorem simp33l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  totprob  34618  cdleme19b  40803  cdleme19d  40805  cdleme19e  40806  cdleme20h  40815  cdleme20l2  40820  cdleme20m  40822  cdleme21d  40829  cdleme21e  40830  cdleme22e  40843  cdleme22f2  40846  cdleme22g  40847  cdleme26e  40858  cdleme28a  40869  cdleme28b  40870  cdleme37m  40961  cdleme39n  40965  cdlemeg46gfre  41031  cdlemg28a  41192  cdlemg28b  41202  cdlemk3  41332  cdlemk5a  41334  cdlemk6  41336  cdlemkuat  41365  cdlemkid2  41423