Theorem simp22r 1378

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

Assertion

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

Proof of Theorem simp22r

Step	Hyp	Ref	Expression
1		simp2r 1243	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1129	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  26034  segconeu  32445  3atlem2  35291  lplnexllnN  35371  lplncvrlvol2  35422  4atex  35883  cdleme3g  36042  cdleme3h  36043  cdleme11h  36074  cdleme20bN  36118  cdleme20c  36119  cdleme20f  36122  cdleme20g  36123  cdleme20j  36126  cdleme20l2  36129  cdleme20l  36130  cdleme21ct  36137  cdleme26e  36167  cdleme43fsv1snlem  36228  cdleme39n  36274  cdleme40m  36275  cdleme42k  36292  cdlemg6c  36428  cdlemg31d  36508  cdlemg33a  36514  cdlemg33c  36516  cdlemg33d  36517  cdlemg33e  36518  cdlemg33  36519  cdlemh  36625  cdlemk7u-2N  36696  cdlemk11u-2N  36697  cdlemk12u-2N  36698  cdlemk20-2N  36700  cdlemk28-3  36716  cdlemk33N  36717  cdlemk34  36718  cdlemk39  36724  cdlemkyyN  36770