Theorem simp22r 1294

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

Assertion

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

Proof of Theorem simp22r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  frrlem10  8274  ttrclselem2  9679  ax5seglem6  28861  segconeu  35999  3atlem2  39478  lplnexllnN  39558  lplncvrlvol2  39609  4atex  40070  cdleme3g  40228  cdleme3h  40229  cdleme11h  40260  cdleme20bN  40304  cdleme20c  40305  cdleme20f  40308  cdleme20g  40309  cdleme20j  40312  cdleme20l2  40315  cdleme20l  40316  cdleme21ct  40323  cdleme26e  40353  cdleme43fsv1snlem  40414  cdleme39n  40460  cdleme40m  40461  cdleme42k  40478  cdlemg6c  40614  cdlemg31d  40694  cdlemg33a  40700  cdlemg33c  40702  cdlemg33d  40703  cdlemg33e  40704  cdlemg33  40705  cdlemh  40811  cdlemk7u-2N  40882  cdlemk11u-2N  40883  cdlemk12u-2N  40884  cdlemk20-2N  40886  cdlemk28-3  40902  cdlemk33N  40903  cdlemk34  40904  cdlemk39  40910  cdlemkyyN  40956