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  39976  cdlema1N  40239  trlval3  40635  cdleme12  40719  cdlemednpq  40747  cdleme19d  40754  cdleme19e  40755  cdleme20f  40762  cdleme20h  40764  cdleme20l2  40769  cdleme20l  40770  cdleme20m  40771  cdleme21j  40784  cdleme22a  40788  cdleme22cN  40790  cdleme22f2  40795  cdleme32b  40890  cdlemg12f  41096  cdlemg12g  41097  cdlemg12  41098  cdlemg28a  41141  cdlemg31b0N  41142  cdlemg29  41153  cdlemg33a  41154  cdlemg36  41162  cdlemg42  41177  cdlemk16a  41304  cdlemk21-2N  41339  cdlemk32  41345  cdlemkid2  41372  cdlemk54  41406  cdlemk55a  41407  dihord10  41671