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  39974  cdlema1N  40237  trlval3  40633  cdleme12  40717  cdlemednpq  40745  cdleme19d  40752  cdleme19e  40753  cdleme20f  40760  cdleme20h  40762  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme21j  40782  cdleme22a  40786  cdleme22cN  40788  cdleme22f2  40793  cdleme32b  40888  cdlemg12f  41094  cdlemg12g  41095  cdlemg12  41096  cdlemg28a  41139  cdlemg31b0N  41140  cdlemg29  41151  cdlemg33a  41152  cdlemg36  41160  cdlemg42  41175  cdlemk16a  41302  cdlemk21-2N  41337  cdlemk32  41343  cdlemkid2  41370  cdlemk54  41404  cdlemk55a  41405  dihord10  41669