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  8233  ttrclselem2  9625  ax5seglem6  28916  segconeu  36078  3atlem2  39606  lplnexllnN  39686  lplncvrlvol2  39737  4atex  40198  cdleme3g  40356  cdleme3h  40357  cdleme11h  40388  cdleme20bN  40432  cdleme20c  40433  cdleme20f  40436  cdleme20g  40437  cdleme20j  40440  cdleme20l2  40443  cdleme20l  40444  cdleme21ct  40451  cdleme26e  40481  cdleme43fsv1snlem  40542  cdleme39n  40588  cdleme40m  40589  cdleme42k  40606  cdlemg6c  40742  cdlemg31d  40822  cdlemg33a  40828  cdlemg33c  40830  cdlemg33d  40831  cdlemg33e  40832  cdlemg33  40833  cdlemh  40939  cdlemk7u-2N  41010  cdlemk11u-2N  41011  cdlemk12u-2N  41012  cdlemk20-2N  41014  cdlemk28-3  41030  cdlemk33N  41031  cdlemk34  41032  cdlemk39  41038  cdlemkyyN  41084