Theorem simp31l 1313

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

Assertion

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

Proof of Theorem simp31l

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ps-2c  40164  cdlema1N  40427  trlval3  40823  cdleme12  40907  cdlemednpq  40935  cdleme19d  40942  cdleme19e  40943  cdleme20f  40950  cdleme20h  40952  cdleme20l2  40957  cdleme20l  40958  cdleme20m  40959  cdleme21j  40972  cdleme22a  40976  cdleme22cN  40978  cdleme22f2  40983  cdleme32b  41078  cdlemg12f  41284  cdlemg12g  41285  cdlemg12  41286  cdlemg28a  41329  cdlemg31b0N  41330  cdlemg29  41341  cdlemg33a  41342  cdlemg36  41350  cdlemg42  41365  cdlemk16a  41492  cdlemk21-2N  41527  cdlemk32  41533  cdlemkid2  41560  cdlemk54  41594  cdlemk55a  41595  dihord10  41859