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  28192  segconeu  34983  3atlem2  38355  lplnexllnN  38435  lplncvrlvol2  38486  4atex  38947  cdleme3g  39105  cdleme3h  39106  cdleme11h  39137  cdleme20bN  39181  cdleme20c  39182  cdleme20f  39185  cdleme20g  39186  cdleme20j  39189  cdleme20l2  39192  cdleme20l  39193  cdleme21ct  39200  cdleme26e  39230  cdleme43fsv1snlem  39291  cdleme39n  39337  cdleme40m  39338  cdleme42k  39355  cdlemg6c  39491  cdlemg31d  39571  cdlemg33a  39577  cdlemg33c  39579  cdlemg33d  39580  cdlemg33e  39581  cdlemg33  39582  cdlemh  39688  cdlemk7u-2N  39759  cdlemk11u-2N  39760  cdlemk12u-2N  39761  cdlemk20-2N  39763  cdlemk28-3  39779  cdlemk33N  39780  cdlemk34  39781  cdlemk39  39787  cdlemkyyN  39833