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  8277  ttrclselem2  9686  ax5seglem6  28868  segconeu  36006  3atlem2  39485  lplnexllnN  39565  lplncvrlvol2  39616  4atex  40077  cdleme3g  40235  cdleme3h  40236  cdleme11h  40267  cdleme20bN  40311  cdleme20c  40312  cdleme20f  40315  cdleme20g  40316  cdleme20j  40319  cdleme20l2  40322  cdleme20l  40323  cdleme21ct  40330  cdleme26e  40360  cdleme43fsv1snlem  40421  cdleme39n  40467  cdleme40m  40468  cdleme42k  40485  cdlemg6c  40621  cdlemg31d  40701  cdlemg33a  40707  cdlemg33c  40709  cdlemg33d  40710  cdlemg33e  40711  cdlemg33  40712  cdlemh  40818  cdlemk7u-2N  40889  cdlemk11u-2N  40890  cdlemk12u-2N  40891  cdlemk20-2N  40893  cdlemk28-3  40909  cdlemk33N  40910  cdlemk34  40911  cdlemk39  40917  cdlemkyyN  40963