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 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:  ps-2c  39507  cdlema1N  39770  trlval3  40166  cdleme12  40250  cdlemednpq  40278  cdleme19d  40285  cdleme19e  40286  cdleme20f  40293  cdleme20h  40295  cdleme20l2  40300  cdleme20l  40301  cdleme20m  40302  cdleme21j  40315  cdleme22a  40319  cdleme22cN  40321  cdleme22f2  40326  cdleme32b  40421  cdlemg12f  40627  cdlemg12g  40628  cdlemg12  40629  cdlemg28a  40672  cdlemg31b0N  40673  cdlemg29  40684  cdlemg33a  40685  cdlemg36  40693  cdlemg42  40708  cdlemk16a  40835  cdlemk21-2N  40870  cdlemk32  40876  cdlemkid2  40903  cdlemk54  40937  cdlemk55a  40938  dihord10  41202