Theorem simp22r 1300

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

Assertion

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

Proof of Theorem simp22r

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

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

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  frrlem10  8242  ttrclselem2  9645  ax5seglem6  29028  segconeu  36246  3atlem2  39983  lplnexllnN  40063  lplncvrlvol2  40114  4atex  40575  cdleme3g  40733  cdleme3h  40734  cdleme11h  40765  cdleme20bN  40809  cdleme20c  40810  cdleme20f  40813  cdleme20g  40814  cdleme20j  40817  cdleme20l2  40820  cdleme20l  40821  cdleme21ct  40828  cdleme26e  40858  cdleme43fsv1snlem  40919  cdleme39n  40965  cdleme40m  40966  cdleme42k  40983  cdlemg6c  41119  cdlemg31d  41199  cdlemg33a  41205  cdlemg33c  41207  cdlemg33d  41208  cdlemg33e  41209  cdlemg33  41210  cdlemh  41316  cdlemk7u-2N  41387  cdlemk11u-2N  41388  cdlemk12u-2N  41389  cdlemk20-2N  41391  cdlemk28-3  41407  cdlemk33N  41408  cdlemk34  41409  cdlemk39  41415  cdlemkyyN  41461