Theorem simp22r 1174

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

Assertion

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

Proof of Theorem simp22r

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  ax5seglem6  25614  segconeu  31288  3atlem2  33788  lplnexllnN  33868  lplncvrlvol2  33919  4atex  34380  cdleme3g  34539  cdleme3h  34540  cdleme11h  34571  cdleme20bN  34616  cdleme20c  34617  cdleme20f  34620  cdleme20g  34621  cdleme20j  34624  cdleme20l2  34627  cdleme20l  34628  cdleme21ct  34635  cdleme26e  34665  cdleme43fsv1snlem  34726  cdleme39n  34772  cdleme40m  34773  cdleme42k  34790  cdlemg6c  34926  cdlemg31d  35006  cdlemg33a  35012  cdlemg33c  35014  cdlemg33d  35015  cdlemg33e  35016  cdlemg33  35017  cdlemh  35123  cdlemk7u-2N  35194  cdlemk11u-2N  35195  cdlemk12u-2N  35196  cdlemk20-2N  35198  cdlemk28-3  35214  cdlemk33N  35215  cdlemk34  35216  cdlemk39  35222  cdlemkyyN  35268