Theorem simp31l 1293

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

Assertion

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

Proof of Theorem simp31l

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  ps-2c  39070  cdlema1N  39333  trlval3  39729  cdleme12  39813  cdlemednpq  39841  cdleme19d  39848  cdleme19e  39849  cdleme20f  39856  cdleme20h  39858  cdleme20l2  39863  cdleme20l  39864  cdleme20m  39865  cdleme21j  39878  cdleme22a  39882  cdleme22cN  39884  cdleme22f2  39889  cdleme32b  39984  cdlemg12f  40190  cdlemg12g  40191  cdlemg12  40192  cdlemg28a  40235  cdlemg31b0N  40236  cdlemg29  40247  cdlemg33a  40248  cdlemg36  40256  cdlemg42  40271  cdlemk16a  40398  cdlemk21-2N  40433  cdlemk32  40439  cdlemkid2  40466  cdlemk54  40500  cdlemk55a  40501  dihord10  40765