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  8237  ttrclselem2  9635  ax5seglem6  29007  segconeu  36205  3atlem2  39744  lplnexllnN  39824  lplncvrlvol2  39875  4atex  40336  cdleme3g  40494  cdleme3h  40495  cdleme11h  40526  cdleme20bN  40570  cdleme20c  40571  cdleme20f  40574  cdleme20g  40575  cdleme20j  40578  cdleme20l2  40581  cdleme20l  40582  cdleme21ct  40589  cdleme26e  40619  cdleme43fsv1snlem  40680  cdleme39n  40726  cdleme40m  40727  cdleme42k  40744  cdlemg6c  40880  cdlemg31d  40960  cdlemg33a  40966  cdlemg33c  40968  cdlemg33d  40969  cdlemg33e  40970  cdlemg33  40971  cdlemh  41077  cdlemk7u-2N  41148  cdlemk11u-2N  41149  cdlemk12u-2N  41150  cdlemk20-2N  41152  cdlemk28-3  41168  cdlemk33N  41169  cdlemk34  41170  cdlemk39  41176  cdlemkyyN  41222