Theorem simp32r 1316

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

Assertion

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

Proof of Theorem simp32r

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

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

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 1103

This theorem is referenced by:  cdlema1N  40455  paddasslem15  40498  4atex2-0aOLDN  40742  4atex3  40745  cdleme19b  40968  cdleme19d  40970  cdleme19e  40971  cdleme20d  40976  cdleme20f  40978  cdleme20g  40979  cdleme21d  40994  cdleme21e  40995  cdleme22cN  41006  cdleme22e  41008  cdleme22f2  41011  cdleme26e  41023  cdleme28a  41034  cdleme37m  41126  cdlemg28b  41367  cdlemk3  41497  cdlemk12  41514  cdlemk12u  41536  cdlemkoatnle-2N  41539  cdlemk13-2N  41540  cdlemkole-2N  41541  cdlemk14-2N  41542  cdlemk15-2N  41543  cdlemk16-2N  41544  cdlemk17-2N  41545  cdlemk18-2N  41550  cdlemk19-2N  41551  cdlemk7u-2N  41552  cdlemk11u-2N  41553  cdlemk20-2N  41556  cdlemk30  41558  cdlemk23-3  41566  cdlemk24-3  41567