Theorem simp32r 1301

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

Assertion

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

Proof of Theorem simp32r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  cdlema1N  40164  paddasslem15  40207  4atex2-0aOLDN  40451  4atex3  40454  cdleme19b  40677  cdleme19d  40679  cdleme19e  40680  cdleme20d  40685  cdleme20f  40687  cdleme20g  40688  cdleme21d  40703  cdleme21e  40704  cdleme22cN  40715  cdleme22e  40717  cdleme22f2  40720  cdleme26e  40732  cdleme28a  40743  cdleme37m  40835  cdlemg28b  41076  cdlemk3  41206  cdlemk12  41223  cdlemk12u  41245  cdlemkoatnle-2N  41248  cdlemk13-2N  41249  cdlemkole-2N  41250  cdlemk14-2N  41251  cdlemk15-2N  41252  cdlemk16-2N  41253  cdlemk17-2N  41254  cdlemk18-2N  41259  cdlemk19-2N  41260  cdlemk7u-2N  41261  cdlemk11u-2N  41262  cdlemk20-2N  41265  cdlemk30  41267  cdlemk23-3  41275  cdlemk24-3  41276