Theorem simp32r 1318

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

Assertion

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

Proof of Theorem simp32r

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

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

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 1105

This theorem is referenced by:  cdlema1N  40546  paddasslem15  40589  4atex2-0aOLDN  40833  4atex3  40836  cdleme19b  41059  cdleme19d  41061  cdleme19e  41062  cdleme20d  41067  cdleme20f  41069  cdleme20g  41070  cdleme21d  41085  cdleme21e  41086  cdleme22cN  41097  cdleme22e  41099  cdleme22f2  41102  cdleme26e  41114  cdleme28a  41125  cdleme37m  41217  cdlemg28b  41458  cdlemk3  41588  cdlemk12  41605  cdlemk12u  41627  cdlemkoatnle-2N  41630  cdlemk13-2N  41631  cdlemkole-2N  41632  cdlemk14-2N  41633  cdlemk15-2N  41634  cdlemk16-2N  41635  cdlemk17-2N  41636  cdlemk18-2N  41641  cdlemk19-2N  41642  cdlemk7u-2N  41643  cdlemk11u-2N  41644  cdlemk20-2N  41647  cdlemk30  41649  cdlemk23-3  41657  cdlemk24-3  41658