Theorem simp22r 1289

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

Assertion

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

Proof of Theorem simp22r

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ax5seglem6  26722  frrlem10  33134  segconeu  33474  3atlem2  36622  lplnexllnN  36702  lplncvrlvol2  36753  4atex  37214  cdleme3g  37372  cdleme3h  37373  cdleme11h  37404  cdleme20bN  37448  cdleme20c  37449  cdleme20f  37452  cdleme20g  37453  cdleme20j  37456  cdleme20l2  37459  cdleme20l  37460  cdleme21ct  37467  cdleme26e  37497  cdleme43fsv1snlem  37558  cdleme39n  37604  cdleme40m  37605  cdleme42k  37622  cdlemg6c  37758  cdlemg31d  37838  cdlemg33a  37844  cdlemg33c  37846  cdlemg33d  37847  cdlemg33e  37848  cdlemg33  37849  cdlemh  37955  cdlemk7u-2N  38026  cdlemk11u-2N  38027  cdlemk12u-2N  38028  cdlemk20-2N  38030  cdlemk28-3  38046  cdlemk33N  38047  cdlemk34  38048  cdlemk39  38054  cdlemkyyN  38100