Theorem simp31l 1296

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

Assertion

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

Proof of Theorem simp31l

Step	Hyp	Ref	Expression
1		simp1l 1197	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant3 1135	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  39485  cdlema1N  39748  trlval3  40144  cdleme12  40228  cdlemednpq  40256  cdleme19d  40263  cdleme19e  40264  cdleme20f  40271  cdleme20h  40273  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme21j  40293  cdleme22a  40297  cdleme22cN  40299  cdleme22f2  40304  cdleme32b  40399  cdlemg12f  40605  cdlemg12g  40606  cdlemg12  40607  cdlemg28a  40650  cdlemg31b0N  40651  cdlemg29  40662  cdlemg33a  40663  cdlemg36  40671  cdlemg42  40686  cdlemk16a  40813  cdlemk21-2N  40848  cdlemk32  40854  cdlemkid2  40881  cdlemk54  40915  cdlemk55a  40916  dihord10  41180