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 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  8319  ttrclselem2  9764  ax5seglem6  28964  segconeu  35993  3atlem2  39467  lplnexllnN  39547  lplncvrlvol2  39598  4atex  40059  cdleme3g  40217  cdleme3h  40218  cdleme11h  40249  cdleme20bN  40293  cdleme20c  40294  cdleme20f  40297  cdleme20g  40298  cdleme20j  40301  cdleme20l2  40304  cdleme20l  40305  cdleme21ct  40312  cdleme26e  40342  cdleme43fsv1snlem  40403  cdleme39n  40449  cdleme40m  40450  cdleme42k  40467  cdlemg6c  40603  cdlemg31d  40683  cdlemg33a  40689  cdlemg33c  40691  cdlemg33d  40692  cdlemg33e  40693  cdlemg33  40694  cdlemh  40800  cdlemk7u-2N  40871  cdlemk11u-2N  40872  cdlemk12u-2N  40873  cdlemk20-2N  40875  cdlemk28-3  40891  cdlemk33N  40892  cdlemk34  40893  cdlemk39  40899  cdlemkyyN  40945