Theorem simp31l 1294

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

Assertion

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

Proof of Theorem simp31l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  ps-2c  37469  cdlema1N  37732  trlval3  38128  cdleme12  38212  cdlemednpq  38240  cdleme19d  38247  cdleme19e  38248  cdleme20f  38255  cdleme20h  38257  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme21j  38277  cdleme22a  38281  cdleme22cN  38283  cdleme22f2  38288  cdleme32b  38383  cdlemg12f  38589  cdlemg12g  38590  cdlemg12  38591  cdlemg28a  38634  cdlemg31b0N  38635  cdlemg29  38646  cdlemg33a  38647  cdlemg36  38655  cdlemg42  38670  cdlemk16a  38797  cdlemk21-2N  38832  cdlemk32  38838  cdlemkid2  38865  cdlemk54  38899  cdlemk55a  38900  dihord10  39164