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 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  ps-2c  40280  cdlema1N  40543  trlval3  40939  cdleme12  41023  cdlemednpq  41051  cdleme19d  41058  cdleme19e  41059  cdleme20f  41066  cdleme20h  41068  cdleme20l2  41073  cdleme20l  41074  cdleme20m  41075  cdleme21j  41088  cdleme22a  41092  cdleme22cN  41094  cdleme22f2  41099  cdleme32b  41194  cdlemg12f  41400  cdlemg12g  41401  cdlemg12  41402  cdlemg28a  41445  cdlemg31b0N  41446  cdlemg29  41457  cdlemg33a  41458  cdlemg36  41466  cdlemg42  41481  cdlemk16a  41608  cdlemk21-2N  41643  cdlemk32  41649  cdlemkid2  41676  cdlemk54  41710  cdlemk55a  41711  dihord10  41975