Theorem simp22r 1295

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

Assertion

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

Proof of Theorem simp22r

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

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

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 1089

This theorem is referenced by:  frrlem10  8247  ttrclselem2  9647  ax5seglem6  29019  segconeu  36224  3atlem2  39857  lplnexllnN  39937  lplncvrlvol2  39988  4atex  40449  cdleme3g  40607  cdleme3h  40608  cdleme11h  40639  cdleme20bN  40683  cdleme20c  40684  cdleme20f  40687  cdleme20g  40688  cdleme20j  40691  cdleme20l2  40694  cdleme20l  40695  cdleme21ct  40702  cdleme26e  40732  cdleme43fsv1snlem  40793  cdleme39n  40839  cdleme40m  40840  cdleme42k  40857  cdlemg6c  40993  cdlemg31d  41073  cdlemg33a  41079  cdlemg33c  41081  cdlemg33d  41082  cdlemg33e  41083  cdlemg33  41084  cdlemh  41190  cdlemk7u-2N  41261  cdlemk11u-2N  41262  cdlemk12u-2N  41263  cdlemk20-2N  41265  cdlemk28-3  41281  cdlemk33N  41282  cdlemk34  41283  cdlemk39  41289  cdlemkyyN  41335