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  8317  ttrclselem2  9731  ax5seglem6  29518  segconeu  36869  3atlem2  40635  lplnexllnN  40715  lplncvrlvol2  40766  4atex  41227  cdleme3g  41385  cdleme3h  41386  cdleme11h  41417  cdleme20bN  41461  cdleme20c  41462  cdleme20f  41465  cdleme20g  41466  cdleme20j  41469  cdleme20l2  41472  cdleme20l  41473  cdleme21ct  41480  cdleme26e  41510  cdleme43fsv1snlem  41571  cdleme39n  41617  cdleme40m  41618  cdleme42k  41635  cdlemg6c  41771  cdlemg31d  41851  cdlemg33a  41857  cdlemg33c  41859  cdlemg33d  41860  cdlemg33e  41861  cdlemg33  41862  cdlemh  41968  cdlemk7u-2N  42039  cdlemk11u-2N  42040  cdlemk12u-2N  42041  cdlemk20-2N  42043  cdlemk28-3  42059  cdlemk33N  42060  cdlemk34  42061  cdlemk39  42067  cdlemkyyN  42113