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  39898  cdlema1N  40161  trlval3  40557  cdleme12  40641  cdlemednpq  40669  cdleme19d  40676  cdleme19e  40677  cdleme20f  40684  cdleme20h  40686  cdleme20l2  40691  cdleme20l  40692  cdleme20m  40693  cdleme21j  40706  cdleme22a  40710  cdleme22cN  40712  cdleme22f2  40717  cdleme32b  40812  cdlemg12f  41018  cdlemg12g  41019  cdlemg12  41020  cdlemg28a  41063  cdlemg31b0N  41064  cdlemg29  41075  cdlemg33a  41076  cdlemg36  41084  cdlemg42  41099  cdlemk16a  41226  cdlemk21-2N  41261  cdlemk32  41267  cdlemkid2  41294  cdlemk54  41328  cdlemk55a  41329  dihord10  41593