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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  ps-2c  38305  cdlema1N  38568  trlval3  38964  cdleme12  39048  cdlemednpq  39076  cdleme19d  39083  cdleme19e  39084  cdleme20f  39091  cdleme20h  39093  cdleme20l2  39098  cdleme20l  39099  cdleme20m  39100  cdleme21j  39113  cdleme22a  39117  cdleme22cN  39119  cdleme22f2  39124  cdleme32b  39219  cdlemg12f  39425  cdlemg12g  39426  cdlemg12  39427  cdlemg28a  39470  cdlemg31b0N  39471  cdlemg29  39482  cdlemg33a  39483  cdlemg36  39491  cdlemg42  39506  cdlemk16a  39633  cdlemk21-2N  39668  cdlemk32  39674  cdlemkid2  39701  cdlemk54  39735  cdlemk55a  39736  dihord10  40000