Theorem simp31l 1297

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

Assertion

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

Proof of Theorem simp31l

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

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

This theorem is referenced by:  ps-2c  39566  cdlema1N  39829  trlval3  40225  cdleme12  40309  cdlemednpq  40337  cdleme19d  40344  cdleme19e  40345  cdleme20f  40352  cdleme20h  40354  cdleme20l2  40359  cdleme20l  40360  cdleme20m  40361  cdleme21j  40374  cdleme22a  40378  cdleme22cN  40380  cdleme22f2  40385  cdleme32b  40480  cdlemg12f  40686  cdlemg12g  40687  cdlemg12  40688  cdlemg28a  40731  cdlemg31b0N  40732  cdlemg29  40743  cdlemg33a  40744  cdlemg36  40752  cdlemg42  40767  cdlemk16a  40894  cdlemk21-2N  40929  cdlemk32  40935  cdlemkid2  40962  cdlemk54  40996  cdlemk55a  40997  dihord10  41261