Theorem simp32r 1295

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

Assertion

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

Proof of Theorem simp32r

Step	Hyp	Ref	Expression
1		simp2r 1196	. 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:  cdlema1N  36942  paddasslem15  36985  4atex2-0aOLDN  37229  4atex3  37232  cdleme19b  37455  cdleme19d  37457  cdleme19e  37458  cdleme20d  37463  cdleme20f  37465  cdleme20g  37466  cdleme21d  37481  cdleme21e  37482  cdleme22cN  37493  cdleme22e  37495  cdleme22f2  37498  cdleme26e  37510  cdleme28a  37521  cdleme37m  37613  cdlemg28b  37854  cdlemk3  37984  cdlemk12  38001  cdlemk12u  38023  cdlemkoatnle-2N  38026  cdlemk13-2N  38027  cdlemkole-2N  38028  cdlemk14-2N  38029  cdlemk15-2N  38030  cdlemk16-2N  38031  cdlemk17-2N  38032  cdlemk18-2N  38037  cdlemk19-2N  38038  cdlemk7u-2N  38039  cdlemk11u-2N  38040  cdlemk20-2N  38043  cdlemk30  38045  cdlemk23-3  38053  cdlemk24-3  38054