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  40553  cdlema1N  40816  trlval3  41212  cdleme12  41296  cdlemednpq  41324  cdleme19d  41331  cdleme19e  41332  cdleme20f  41339  cdleme20h  41341  cdleme20l2  41346  cdleme20l  41347  cdleme20m  41348  cdleme21j  41361  cdleme22a  41365  cdleme22cN  41367  cdleme22f2  41372  cdleme32b  41467  cdlemg12f  41673  cdlemg12g  41674  cdlemg12  41675  cdlemg28a  41718  cdlemg31b0N  41719  cdlemg29  41730  cdlemg33a  41731  cdlemg36  41739  cdlemg42  41754  cdlemk16a  41881  cdlemk21-2N  41916  cdlemk32  41922  cdlemkid2  41949  cdlemk54  41983  cdlemk55a  41984  dihord10  42248