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 1134	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  frrlem10  8225  ttrclselem2  9616  ax5seglem6  28913  segconeu  36051  3atlem2  39529  lplnexllnN  39609  lplncvrlvol2  39660  4atex  40121  cdleme3g  40279  cdleme3h  40280  cdleme11h  40311  cdleme20bN  40355  cdleme20c  40356  cdleme20f  40359  cdleme20g  40360  cdleme20j  40363  cdleme20l2  40366  cdleme20l  40367  cdleme21ct  40374  cdleme26e  40404  cdleme43fsv1snlem  40465  cdleme39n  40511  cdleme40m  40512  cdleme42k  40529  cdlemg6c  40665  cdlemg31d  40745  cdlemg33a  40751  cdlemg33c  40753  cdlemg33d  40754  cdlemg33e  40755  cdlemg33  40756  cdlemh  40862  cdlemk7u-2N  40933  cdlemk11u-2N  40934  cdlemk12u-2N  40935  cdlemk20-2N  40937  cdlemk28-3  40953  cdlemk33N  40954  cdlemk34  40955  cdlemk39  40961  cdlemkyyN  41007