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  29321  segconeu  36524  3atlem2  40299  lplnexllnN  40379  lplncvrlvol2  40430  4atex  40891  cdleme3g  41049  cdleme3h  41050  cdleme11h  41081  cdleme20bN  41125  cdleme20c  41126  cdleme20f  41129  cdleme20g  41130  cdleme20j  41133  cdleme20l2  41136  cdleme20l  41137  cdleme21ct  41144  cdleme26e  41174  cdleme43fsv1snlem  41235  cdleme39n  41281  cdleme40m  41282  cdleme42k  41299  cdlemg6c  41435  cdlemg31d  41515  cdlemg33a  41521  cdlemg33c  41523  cdlemg33d  41524  cdlemg33e  41525  cdlemg33  41526  cdlemh  41632  cdlemk7u-2N  41703  cdlemk11u-2N  41704  cdlemk12u-2N  41705  cdlemk20-2N  41707  cdlemk28-3  41723  cdlemk33N  41724  cdlemk34  41725  cdlemk39  41731  cdlemkyyN  41777