Theorem simp22r 1290

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

Assertion

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

Proof of Theorem simp22r

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

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

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  ax5seglem6  26728  frrlem10  33245  segconeu  33585  3atlem2  36780  lplnexllnN  36860  lplncvrlvol2  36911  4atex  37372  cdleme3g  37530  cdleme3h  37531  cdleme11h  37562  cdleme20bN  37606  cdleme20c  37607  cdleme20f  37610  cdleme20g  37611  cdleme20j  37614  cdleme20l2  37617  cdleme20l  37618  cdleme21ct  37625  cdleme26e  37655  cdleme43fsv1snlem  37716  cdleme39n  37762  cdleme40m  37763  cdleme42k  37780  cdlemg6c  37916  cdlemg31d  37996  cdlemg33a  38002  cdlemg33c  38004  cdlemg33d  38005  cdlemg33e  38006  cdlemg33  38007  cdlemh  38113  cdlemk7u-2N  38184  cdlemk11u-2N  38185  cdlemk12u-2N  38186  cdlemk20-2N  38188  cdlemk28-3  38204  cdlemk33N  38205  cdlemk34  38206  cdlemk39  38212  cdlemkyyN  38258