Theorem simp22r 1291

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

Assertion

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

Proof of Theorem simp22r

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  frrlem10  8082  ax5seglem6  27205  ttrclselem2  33712  segconeu  34240  3atlem2  37425  lplnexllnN  37505  lplncvrlvol2  37556  4atex  38017  cdleme3g  38175  cdleme3h  38176  cdleme11h  38207  cdleme20bN  38251  cdleme20c  38252  cdleme20f  38255  cdleme20g  38256  cdleme20j  38259  cdleme20l2  38262  cdleme20l  38263  cdleme21ct  38270  cdleme26e  38300  cdleme43fsv1snlem  38361  cdleme39n  38407  cdleme40m  38408  cdleme42k  38425  cdlemg6c  38561  cdlemg31d  38641  cdlemg33a  38647  cdlemg33c  38649  cdlemg33d  38650  cdlemg33e  38651  cdlemg33  38652  cdlemh  38758  cdlemk7u-2N  38829  cdlemk11u-2N  38830  cdlemk12u-2N  38831  cdlemk20-2N  38833  cdlemk28-3  38849  cdlemk33N  38850  cdlemk34  38851  cdlemk39  38857  cdlemkyyN  38903