Theorem simp22r 1385

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

Assertion

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

Proof of Theorem simp22r

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

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

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  ax5seglem6  26028  segconeu  32439  3atlem2  35264  lplnexllnN  35344  lplncvrlvol2  35395  4atex  35856  cdleme3g  36015  cdleme3h  36016  cdleme11h  36047  cdleme20bN  36091  cdleme20c  36092  cdleme20f  36095  cdleme20g  36096  cdleme20j  36099  cdleme20l2  36102  cdleme20l  36103  cdleme21ct  36110  cdleme26e  36140  cdleme43fsv1snlem  36201  cdleme39n  36247  cdleme40m  36248  cdleme42k  36265  cdlemg6c  36401  cdlemg31d  36481  cdlemg33a  36487  cdlemg33c  36489  cdlemg33d  36490  cdlemg33e  36491  cdlemg33  36492  cdlemh  36598  cdlemk7u-2N  36669  cdlemk11u-2N  36670  cdlemk12u-2N  36671  cdlemk20-2N  36673  cdlemk28-3  36689  cdlemk33N  36690  cdlemk34  36691  cdlemk39  36697  cdlemkyyN  36743