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 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  cdlema1N  40598  paddasslem15  40641  4atex2-0aOLDN  40885  4atex3  40888  cdleme19b  41111  cdleme19d  41113  cdleme19e  41114  cdleme20d  41119  cdleme20f  41121  cdleme20g  41122  cdleme21d  41137  cdleme21e  41138  cdleme22cN  41149  cdleme22e  41151  cdleme22f2  41154  cdleme26e  41166  cdleme28a  41177  cdleme37m  41269  cdlemg28b  41510  cdlemk3  41640  cdlemk12  41657  cdlemk12u  41679  cdlemkoatnle-2N  41682  cdlemk13-2N  41683  cdlemkole-2N  41684  cdlemk14-2N  41685  cdlemk15-2N  41686  cdlemk16-2N  41687  cdlemk17-2N  41688  cdlemk18-2N  41693  cdlemk19-2N  41694  cdlemk7u-2N  41695  cdlemk11u-2N  41696  cdlemk20-2N  41699  cdlemk30  41701  cdlemk23-3  41709  cdlemk24-3  41710