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  8344  ttrclselem2  9757  ax5seglem6  29545  segconeu  36967  3atlem2  40744  lplnexllnN  40824  lplncvrlvol2  40875  4atex  41336  cdleme3g  41494  cdleme3h  41495  cdleme11h  41526  cdleme20bN  41570  cdleme20c  41571  cdleme20f  41574  cdleme20g  41575  cdleme20j  41578  cdleme20l2  41581  cdleme20l  41582  cdleme21ct  41589  cdleme26e  41619  cdleme43fsv1snlem  41680  cdleme39n  41726  cdleme40m  41727  cdleme42k  41744  cdlemg6c  41880  cdlemg31d  41960  cdlemg33a  41966  cdlemg33c  41968  cdlemg33d  41969  cdlemg33e  41970  cdlemg33  41971  cdlemh  42077  cdlemk7u-2N  42148  cdlemk11u-2N  42149  cdlemk12u-2N  42150  cdlemk20-2N  42152  cdlemk28-3  42168  cdlemk33N  42169  cdlemk34  42170  cdlemk39  42176  cdlemkyyN  42222