Theorem simp22r 1375

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

Assertion

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

Proof of Theorem simp22r

Step	Hyp	Ref	Expression
1		simp2r 1240	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1128	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  ax5seglem6  26005  segconeu  32416  3atlem2  35265  lplnexllnN  35345  lplncvrlvol2  35396  4atex  35857  cdleme3g  36016  cdleme3h  36017  cdleme11h  36048  cdleme20bN  36092  cdleme20c  36093  cdleme20f  36096  cdleme20g  36097  cdleme20j  36100  cdleme20l2  36103  cdleme20l  36104  cdleme21ct  36111  cdleme26e  36141  cdleme43fsv1snlem  36202  cdleme39n  36248  cdleme40m  36249  cdleme42k  36266  cdlemg6c  36402  cdlemg31d  36482  cdlemg33a  36488  cdlemg33c  36490  cdlemg33d  36491  cdlemg33e  36492  cdlemg33  36493  cdlemh  36599  cdlemk7u-2N  36670  cdlemk11u-2N  36671  cdlemk12u-2N  36672  cdlemk20-2N  36674  cdlemk28-3  36690  cdlemk33N  36691  cdlemk34  36692  cdlemk39  36698  cdlemkyyN  36744