Theorem simp31l 1315

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

Assertion

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

Proof of Theorem simp31l

Step	Hyp	Ref	Expression
1		simp1l 1216	. 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:  ps-2c  40409  cdlema1N  40672  trlval3  41068  cdleme12  41152  cdlemednpq  41180  cdleme19d  41187  cdleme19e  41188  cdleme20f  41195  cdleme20h  41197  cdleme20l2  41202  cdleme20l  41203  cdleme20m  41204  cdleme21j  41217  cdleme22a  41221  cdleme22cN  41223  cdleme22f2  41228  cdleme32b  41323  cdlemg12f  41529  cdlemg12g  41530  cdlemg12  41531  cdlemg28a  41574  cdlemg31b0N  41575  cdlemg29  41586  cdlemg33a  41587  cdlemg36  41595  cdlemg42  41610  cdlemk16a  41737  cdlemk21-2N  41772  cdlemk32  41778  cdlemkid2  41805  cdlemk54  41839  cdlemk55a  41840  dihord10  42104