Theorem simp31l 1295

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

Assertion

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

Proof of Theorem simp31l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ps-2c  37542  cdlema1N  37805  trlval3  38201  cdleme12  38285  cdlemednpq  38313  cdleme19d  38320  cdleme19e  38321  cdleme20f  38328  cdleme20h  38330  cdleme20l2  38335  cdleme20l  38336  cdleme20m  38337  cdleme21j  38350  cdleme22a  38354  cdleme22cN  38356  cdleme22f2  38361  cdleme32b  38456  cdlemg12f  38662  cdlemg12g  38663  cdlemg12  38664  cdlemg28a  38707  cdlemg31b0N  38708  cdlemg29  38719  cdlemg33a  38720  cdlemg36  38728  cdlemg42  38743  cdlemk16a  38870  cdlemk21-2N  38905  cdlemk32  38911  cdlemkid2  38938  cdlemk54  38972  cdlemk55a  38973  dihord10  39237