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  39647  cdlema1N  39910  trlval3  40306  cdleme12  40390  cdlemednpq  40418  cdleme19d  40425  cdleme19e  40426  cdleme20f  40433  cdleme20h  40435  cdleme20l2  40440  cdleme20l  40441  cdleme20m  40442  cdleme21j  40455  cdleme22a  40459  cdleme22cN  40461  cdleme22f2  40466  cdleme32b  40561  cdlemg12f  40767  cdlemg12g  40768  cdlemg12  40769  cdlemg28a  40812  cdlemg31b0N  40813  cdlemg29  40824  cdlemg33a  40825  cdlemg36  40833  cdlemg42  40848  cdlemk16a  40975  cdlemk21-2N  41010  cdlemk32  41016  cdlemkid2  41043  cdlemk54  41077  cdlemk55a  41078  dihord10  41342