Theorem simp32l 1315

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

Assertion

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

Proof of Theorem simp32l

Step	Hyp	Ref	Expression
1		simp2l 1216	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜑)
2	1	3ad2ant3 1151	1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  cdlema1N  40427  paddasslem15  40470  4atex2-0aOLDN  40714  4atex3  40717  trlval3  40823  cdleme12  40907  cdleme19b  40940  cdleme19d  40942  cdleme19e  40943  cdleme20d  40948  cdleme20f  40950  cdleme20g  40951  cdleme21d  40966  cdleme21e  40967  cdleme21f  40968  cdleme22cN  40978  cdleme22e  40980  cdleme22f2  40983  cdleme22g  40984  cdleme26e  40995  cdleme28a  41006  cdleme37m  41098  cdleme39n  41102  cdlemg28b  41339  cdlemk3  41469  cdlemk12  41486  cdlemk12u  41508  cdlemkoatnle-2N  41511  cdlemk13-2N  41512  cdlemkole-2N  41513  cdlemk14-2N  41514  cdlemk15-2N  41515  cdlemk16-2N  41516  cdlemk17-2N  41517  cdlemk18-2N  41522  cdlemk19-2N  41523  cdlemk7u-2N  41524  cdlemk11u-2N  41525  cdlemk20-2N  41528  cdlemk30  41530  cdlemk23-3  41538  cdlemk24-3  41539