Theorem simp31l 1177

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

Assertion

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

Proof of Theorem simp31l

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  ps-2c  33832  cdlema1N  34095  trlval3  34492  cdleme12  34576  cdlemednpq  34604  cdleme19d  34612  cdleme19e  34613  cdleme20f  34620  cdleme20h  34622  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme21j  34642  cdleme22a  34646  cdleme22cN  34648  cdleme22f2  34653  cdleme32b  34748  cdlemg12f  34954  cdlemg12g  34955  cdlemg12  34956  cdlemg28a  34999  cdlemg31b0N  35000  cdlemg29  35011  cdlemg33a  35012  cdlemg36  35020  cdlemg42  35035  cdlemk16a  35162  cdlemk21-2N  35197  cdlemk32  35203  cdlemkid2  35230  cdlemk54  35264  cdlemk55a  35265  dihord10  35530