Theorem simp31l 1298

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

Assertion

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

Proof of Theorem simp31l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 400  df-3an 1091

This theorem is referenced by:  ps-2c  37279  cdlema1N  37542  trlval3  37938  cdleme12  38022  cdlemednpq  38050  cdleme19d  38057  cdleme19e  38058  cdleme20f  38065  cdleme20h  38067  cdleme20l2  38072  cdleme20l  38073  cdleme20m  38074  cdleme21j  38087  cdleme22a  38091  cdleme22cN  38093  cdleme22f2  38098  cdleme32b  38193  cdlemg12f  38399  cdlemg12g  38400  cdlemg12  38401  cdlemg28a  38444  cdlemg31b0N  38445  cdlemg29  38456  cdlemg33a  38457  cdlemg36  38465  cdlemg42  38480  cdlemk16a  38607  cdlemk21-2N  38642  cdlemk32  38648  cdlemkid2  38675  cdlemk54  38709  cdlemk55a  38710  dihord10  38974