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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ps-2c  39988  cdlema1N  40251  trlval3  40647  cdleme12  40731  cdlemednpq  40759  cdleme19d  40766  cdleme19e  40767  cdleme20f  40774  cdleme20h  40776  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme21j  40796  cdleme22a  40800  cdleme22cN  40802  cdleme22f2  40807  cdleme32b  40902  cdlemg12f  41108  cdlemg12g  41109  cdlemg12  41110  cdlemg28a  41153  cdlemg31b0N  41154  cdlemg29  41165  cdlemg33a  41166  cdlemg36  41174  cdlemg42  41189  cdlemk16a  41316  cdlemk21-2N  41351  cdlemk32  41357  cdlemkid2  41384  cdlemk54  41418  cdlemk55a  41419  dihord10  41683