Theorem simp31l 1303

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

Assertion

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

Proof of Theorem simp31l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ps-2c  40027  cdlema1N  40290  trlval3  40686  cdleme12  40770  cdlemednpq  40798  cdleme19d  40805  cdleme19e  40806  cdleme20f  40813  cdleme20h  40815  cdleme20l2  40820  cdleme20l  40821  cdleme20m  40822  cdleme21j  40835  cdleme22a  40839  cdleme22cN  40841  cdleme22f2  40846  cdleme32b  40941  cdlemg12f  41147  cdlemg12g  41148  cdlemg12  41149  cdlemg28a  41192  cdlemg31b0N  41193  cdlemg29  41204  cdlemg33a  41205  cdlemg36  41213  cdlemg42  41228  cdlemk16a  41355  cdlemk21-2N  41390  cdlemk32  41396  cdlemkid2  41423  cdlemk54  41457  cdlemk55a  41458  dihord10  41722