Theorem simp22r 1292

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

Assertion

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

Proof of Theorem simp22r

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

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

This theorem is referenced by:  frrlem10  8111  ttrclselem2  9484  ax5seglem6  27302  segconeu  34313  3atlem2  37498  lplnexllnN  37578  lplncvrlvol2  37629  4atex  38090  cdleme3g  38248  cdleme3h  38249  cdleme11h  38280  cdleme20bN  38324  cdleme20c  38325  cdleme20f  38328  cdleme20g  38329  cdleme20j  38332  cdleme20l2  38335  cdleme20l  38336  cdleme21ct  38343  cdleme26e  38373  cdleme43fsv1snlem  38434  cdleme39n  38480  cdleme40m  38481  cdleme42k  38498  cdlemg6c  38634  cdlemg31d  38714  cdlemg33a  38720  cdlemg33c  38722  cdlemg33d  38723  cdlemg33e  38724  cdlemg33  38725  cdlemh  38831  cdlemk7u-2N  38902  cdlemk11u-2N  38903  cdlemk12u-2N  38904  cdlemk20-2N  38906  cdlemk28-3  38922  cdlemk33N  38923  cdlemk34  38924  cdlemk39  38930  cdlemkyyN  38976