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  8298  ttrclselem2  9709  ax5seglem6  29399  segconeu  36599  3atlem2  40365  lplnexllnN  40445  lplncvrlvol2  40496  4atex  40957  cdleme3g  41115  cdleme3h  41116  cdleme11h  41147  cdleme20bN  41191  cdleme20c  41192  cdleme20f  41195  cdleme20g  41196  cdleme20j  41199  cdleme20l2  41202  cdleme20l  41203  cdleme21ct  41210  cdleme26e  41240  cdleme43fsv1snlem  41301  cdleme39n  41347  cdleme40m  41348  cdleme42k  41365  cdlemg6c  41501  cdlemg31d  41581  cdlemg33a  41587  cdlemg33c  41589  cdlemg33d  41590  cdlemg33e  41591  cdlemg33  41592  cdlemh  41698  cdlemk7u-2N  41769  cdlemk11u-2N  41770  cdlemk12u-2N  41771  cdlemk20-2N  41773  cdlemk28-3  41789  cdlemk33N  41790  cdlemk34  41791  cdlemk39  41797  cdlemkyyN  41843