Theorem simp22r 1292

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

Assertion

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

Proof of Theorem simp22r

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  frrlem10  8109  ttrclselem2  9482  ax5seglem6  27300  segconeu  34310  3atlem2  37495  lplnexllnN  37575  lplncvrlvol2  37626  4atex  38087  cdleme3g  38245  cdleme3h  38246  cdleme11h  38277  cdleme20bN  38321  cdleme20c  38322  cdleme20f  38325  cdleme20g  38326  cdleme20j  38329  cdleme20l2  38332  cdleme20l  38333  cdleme21ct  38340  cdleme26e  38370  cdleme43fsv1snlem  38431  cdleme39n  38477  cdleme40m  38478  cdleme42k  38495  cdlemg6c  38631  cdlemg31d  38711  cdlemg33a  38717  cdlemg33c  38719  cdlemg33d  38720  cdlemg33e  38721  cdlemg33  38722  cdlemh  38828  cdlemk7u-2N  38899  cdlemk11u-2N  38900  cdlemk12u-2N  38901  cdlemk20-2N  38903  cdlemk28-3  38919  cdlemk33N  38920  cdlemk34  38921  cdlemk39  38927  cdlemkyyN  38973