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  40678  cdlema1N  40941  trlval3  41337  cdleme12  41421  cdlemednpq  41449  cdleme19d  41456  cdleme19e  41457  cdleme20f  41464  cdleme20h  41466  cdleme20l2  41471  cdleme20l  41472  cdleme20m  41473  cdleme21j  41486  cdleme22a  41490  cdleme22cN  41492  cdleme22f2  41497  cdleme32b  41592  cdlemg12f  41798  cdlemg12g  41799  cdlemg12  41800  cdlemg28a  41843  cdlemg31b0N  41844  cdlemg29  41855  cdlemg33a  41856  cdlemg36  41864  cdlemg42  41879  cdlemk16a  42006  cdlemk21-2N  42041  cdlemk32  42047  cdlemkid2  42074  cdlemk54  42108  cdlemk55a  42109  dihord10  42373