Theorem simp22r 1273

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

Assertion

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

Proof of Theorem simp22r

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  ax5seglem6  26423  frrlem10  32659  segconeu  32999  3atlem2  36071  lplnexllnN  36151  lplncvrlvol2  36202  4atex  36663  cdleme3g  36821  cdleme3h  36822  cdleme11h  36853  cdleme20bN  36897  cdleme20c  36898  cdleme20f  36901  cdleme20g  36902  cdleme20j  36905  cdleme20l2  36908  cdleme20l  36909  cdleme21ct  36916  cdleme26e  36946  cdleme43fsv1snlem  37007  cdleme39n  37053  cdleme40m  37054  cdleme42k  37071  cdlemg6c  37207  cdlemg31d  37287  cdlemg33a  37293  cdlemg33c  37295  cdlemg33d  37296  cdlemg33e  37297  cdlemg33  37298  cdlemh  37404  cdlemk7u-2N  37475  cdlemk11u-2N  37476  cdlemk12u-2N  37477  cdlemk20-2N  37479  cdlemk28-3  37495  cdlemk33N  37496  cdlemk34  37497  cdlemk39  37503  cdlemkyyN  37549