Theorem simp31l 1292

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

Assertion

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

Proof of Theorem simp31l

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ps-2c  36666  cdlema1N  36929  trlval3  37325  cdleme12  37409  cdlemednpq  37437  cdleme19d  37444  cdleme19e  37445  cdleme20f  37452  cdleme20h  37454  cdleme20l2  37459  cdleme20l  37460  cdleme20m  37461  cdleme21j  37474  cdleme22a  37478  cdleme22cN  37480  cdleme22f2  37485  cdleme32b  37580  cdlemg12f  37786  cdlemg12g  37787  cdlemg12  37788  cdlemg28a  37831  cdlemg31b0N  37832  cdlemg29  37843  cdlemg33a  37844  cdlemg36  37852  cdlemg42  37867  cdlemk16a  37994  cdlemk21-2N  38029  cdlemk32  38035  cdlemkid2  38062  cdlemk54  38096  cdlemk55a  38097  dihord10  38361