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  8294  ttrclselem2  9740  ax5seglem6  28913  segconeu  36029  3atlem2  39503  lplnexllnN  39583  lplncvrlvol2  39634  4atex  40095  cdleme3g  40253  cdleme3h  40254  cdleme11h  40285  cdleme20bN  40329  cdleme20c  40330  cdleme20f  40333  cdleme20g  40334  cdleme20j  40337  cdleme20l2  40340  cdleme20l  40341  cdleme21ct  40348  cdleme26e  40378  cdleme43fsv1snlem  40439  cdleme39n  40485  cdleme40m  40486  cdleme42k  40503  cdlemg6c  40639  cdlemg31d  40719  cdlemg33a  40725  cdlemg33c  40727  cdlemg33d  40728  cdlemg33e  40729  cdlemg33  40730  cdlemh  40836  cdlemk7u-2N  40907  cdlemk11u-2N  40908  cdlemk12u-2N  40909  cdlemk20-2N  40911  cdlemk28-3  40927  cdlemk33N  40928  cdlemk34  40929  cdlemk39  40935  cdlemkyyN  40981