Theorem simp22r 1294

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

Assertion

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

Proof of Theorem simp22r

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  frrlem10  8280  ttrclselem2  9721  ax5seglem6  28223  segconeu  35014  3atlem2  38403  lplnexllnN  38483  lplncvrlvol2  38534  4atex  38995  cdleme3g  39153  cdleme3h  39154  cdleme11h  39185  cdleme20bN  39229  cdleme20c  39230  cdleme20f  39233  cdleme20g  39234  cdleme20j  39237  cdleme20l2  39240  cdleme20l  39241  cdleme21ct  39248  cdleme26e  39278  cdleme43fsv1snlem  39339  cdleme39n  39385  cdleme40m  39386  cdleme42k  39403  cdlemg6c  39539  cdlemg31d  39619  cdlemg33a  39625  cdlemg33c  39627  cdlemg33d  39628  cdlemg33e  39629  cdlemg33  39630  cdlemh  39736  cdlemk7u-2N  39807  cdlemk11u-2N  39808  cdlemk12u-2N  39809  cdlemk20-2N  39811  cdlemk28-3  39827  cdlemk33N  39828  cdlemk34  39829  cdlemk39  39835  cdlemkyyN  39881