Theorem simp31l 1380

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

Assertion

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

Proof of Theorem simp31l

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  ps-2c  35336  cdlema1N  35599  trlval3  35996  cdleme12  36080  cdlemednpq  36108  cdleme19d  36115  cdleme19e  36116  cdleme20f  36123  cdleme20h  36125  cdleme20l2  36130  cdleme20l  36131  cdleme20m  36132  cdleme21j  36145  cdleme22a  36149  cdleme22cN  36151  cdleme22f2  36156  cdleme32b  36251  cdlemg12f  36457  cdlemg12g  36458  cdlemg12  36459  cdlemg28a  36502  cdlemg31b0N  36503  cdlemg29  36514  cdlemg33a  36515  cdlemg36  36523  cdlemg42  36538  cdlemk16a  36665  cdlemk21-2N  36700  cdlemk32  36706  cdlemkid2  36733  cdlemk54  36767  cdlemk55a  36768  dihord10  37033