Theorem simp32r 1180

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

Assertion

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

Proof of Theorem simp32r

Step	Hyp	Ref	Expression
1		simp2r 1081	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant3 1077	1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  cdlema1N  34095  paddasslem15  34138  4atex2-0aOLDN  34382  4atex3  34385  cdleme19b  34610  cdleme19d  34612  cdleme19e  34613  cdleme20d  34618  cdleme20f  34620  cdleme20g  34621  cdleme21d  34636  cdleme21e  34637  cdleme22cN  34648  cdleme22e  34650  cdleme22f2  34653  cdleme26e  34665  cdleme28a  34676  cdleme37m  34768  cdlemg28b  35009  cdlemk3  35139  cdlemk12  35156  cdlemk12u  35178  cdlemkoatnle-2N  35181  cdlemk13-2N  35182  cdlemkole-2N  35183  cdlemk14-2N  35184  cdlemk15-2N  35185  cdlemk16-2N  35186  cdlemk17-2N  35187  cdlemk18-2N  35192  cdlemk19-2N  35193  cdlemk7u-2N  35194  cdlemk11u-2N  35195  cdlemk20-2N  35198  cdlemk30  35200  cdlemk23-3  35208  cdlemk24-3  35209