Theorem simp22r 1312

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

Assertion

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

Proof of Theorem simp22r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  frrlem10  8301  ttrclselem2  9705  ax5seglem6  29314  segconeu  36516  3atlem2  40291  lplnexllnN  40371  lplncvrlvol2  40422  4atex  40883  cdleme3g  41041  cdleme3h  41042  cdleme11h  41073  cdleme20bN  41117  cdleme20c  41118  cdleme20f  41121  cdleme20g  41122  cdleme20j  41125  cdleme20l2  41128  cdleme20l  41129  cdleme21ct  41136  cdleme26e  41166  cdleme43fsv1snlem  41227  cdleme39n  41273  cdleme40m  41274  cdleme42k  41291  cdlemg6c  41427  cdlemg31d  41507  cdlemg33a  41513  cdlemg33c  41515  cdlemg33d  41516  cdlemg33e  41517  cdlemg33  41518  cdlemh  41624  cdlemk7u-2N  41695  cdlemk11u-2N  41696  cdlemk12u-2N  41697  cdlemk20-2N  41699  cdlemk28-3  41715  cdlemk33N  41716  cdlemk34  41717  cdlemk39  41723  cdlemkyyN  41769