Theorem simp22r 1306

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

Assertion

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

Proof of Theorem simp22r

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  frrlem10  8269  ttrclselem2  9674  ax5seglem6  29091  segconeu  36321  3atlem2  40068  lplnexllnN  40148  lplncvrlvol2  40199  4atex  40660  cdleme3g  40818  cdleme3h  40819  cdleme11h  40850  cdleme20bN  40894  cdleme20c  40895  cdleme20f  40898  cdleme20g  40899  cdleme20j  40902  cdleme20l2  40905  cdleme20l  40906  cdleme21ct  40913  cdleme26e  40943  cdleme43fsv1snlem  41004  cdleme39n  41050  cdleme40m  41051  cdleme42k  41068  cdlemg6c  41204  cdlemg31d  41284  cdlemg33a  41290  cdlemg33c  41292  cdlemg33d  41293  cdlemg33e  41294  cdlemg33  41295  cdlemh  41401  cdlemk7u-2N  41472  cdlemk11u-2N  41473  cdlemk12u-2N  41474  cdlemk20-2N  41476  cdlemk28-3  41492  cdlemk33N  41493  cdlemk34  41494  cdlemk39  41500  cdlemkyyN  41546