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 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is referenced by:  frrlem10  8293  ttrclselem2  9696  ax5seglem6  29265  segconeu  36484  3atlem2  40239  lplnexllnN  40319  lplncvrlvol2  40370  4atex  40831  cdleme3g  40989  cdleme3h  40990  cdleme11h  41021  cdleme20bN  41065  cdleme20c  41066  cdleme20f  41069  cdleme20g  41070  cdleme20j  41073  cdleme20l2  41076  cdleme20l  41077  cdleme21ct  41084  cdleme26e  41114  cdleme43fsv1snlem  41175  cdleme39n  41221  cdleme40m  41222  cdleme42k  41239  cdlemg6c  41375  cdlemg31d  41455  cdlemg33a  41461  cdlemg33c  41463  cdlemg33d  41464  cdlemg33e  41465  cdlemg33  41466  cdlemh  41572  cdlemk7u-2N  41643  cdlemk11u-2N  41644  cdlemk12u-2N  41645  cdlemk20-2N  41647  cdlemk28-3  41663  cdlemk33N  41664  cdlemk34  41665  cdlemk39  41671  cdlemkyyN  41717