Theorem simp31l 1297

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

Assertion

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

Proof of Theorem simp31l

Step	Hyp	Ref	Expression
1		simp1l 1198	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant3 1136	1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  ps-2c  38399  cdlema1N  38662  trlval3  39058  cdleme12  39142  cdlemednpq  39170  cdleme19d  39177  cdleme19e  39178  cdleme20f  39185  cdleme20h  39187  cdleme20l2  39192  cdleme20l  39193  cdleme20m  39194  cdleme21j  39207  cdleme22a  39211  cdleme22cN  39213  cdleme22f2  39218  cdleme32b  39313  cdlemg12f  39519  cdlemg12g  39520  cdlemg12  39521  cdlemg28a  39564  cdlemg31b0N  39565  cdlemg29  39576  cdlemg33a  39577  cdlemg36  39585  cdlemg42  39600  cdlemk16a  39727  cdlemk21-2N  39762  cdlemk32  39768  cdlemkid2  39795  cdlemk54  39829  cdlemk55a  39830  dihord10  40094