Theorem simp32r 1312

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

Assertion

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

Proof of Theorem simp32r

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  cdlema1N  40375  paddasslem15  40418  4atex2-0aOLDN  40662  4atex3  40665  cdleme19b  40888  cdleme19d  40890  cdleme19e  40891  cdleme20d  40896  cdleme20f  40898  cdleme20g  40899  cdleme21d  40914  cdleme21e  40915  cdleme22cN  40926  cdleme22e  40928  cdleme22f2  40931  cdleme26e  40943  cdleme28a  40954  cdleme37m  41046  cdlemg28b  41287  cdlemk3  41417  cdlemk12  41434  cdlemk12u  41456  cdlemkoatnle-2N  41459  cdlemk13-2N  41460  cdlemkole-2N  41461  cdlemk14-2N  41462  cdlemk15-2N  41463  cdlemk16-2N  41464  cdlemk17-2N  41465  cdlemk18-2N  41470  cdlemk19-2N  41471  cdlemk7u-2N  41472  cdlemk11u-2N  41473  cdlemk20-2N  41476  cdlemk30  41478  cdlemk23-3  41486  cdlemk24-3  41487