Theorem simp22r 1179

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp22r	⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓)

Proof of Theorem simp22r

Step	Hyp	Ref	Expression
1		simp2r 1086	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1081	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  ax5seglem6  25709  segconeu  31752  3atlem2  34236  lplnexllnN  34316  lplncvrlvol2  34367  4atex  34828  cdleme3g  34987  cdleme3h  34988  cdleme11h  35019  cdleme20bN  35064  cdleme20c  35065  cdleme20f  35068  cdleme20g  35069  cdleme20j  35072  cdleme20l2  35075  cdleme20l  35076  cdleme21ct  35083  cdleme26e  35113  cdleme43fsv1snlem  35174  cdleme39n  35220  cdleme40m  35221  cdleme42k  35238  cdlemg6c  35374  cdlemg31d  35454  cdlemg33a  35460  cdlemg33c  35462  cdlemg33d  35463  cdlemg33e  35464  cdlemg33  35465  cdlemh  35571  cdlemk7u-2N  35642  cdlemk11u-2N  35643  cdlemk12u-2N  35644  cdlemk20-2N  35646  cdlemk28-3  35662  cdlemk33N  35663  cdlemk34  35664  cdlemk39  35670  cdlemkyyN  35716