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  8228  ttrclselem2  9622  ax5seglem6  28879  segconeu  35995  3atlem2  39473  lplnexllnN  39553  lplncvrlvol2  39604  4atex  40065  cdleme3g  40223  cdleme3h  40224  cdleme11h  40255  cdleme20bN  40299  cdleme20c  40300  cdleme20f  40303  cdleme20g  40304  cdleme20j  40307  cdleme20l2  40310  cdleme20l  40311  cdleme21ct  40318  cdleme26e  40348  cdleme43fsv1snlem  40409  cdleme39n  40455  cdleme40m  40456  cdleme42k  40473  cdlemg6c  40609  cdlemg31d  40689  cdlemg33a  40695  cdlemg33c  40697  cdlemg33d  40698  cdlemg33e  40699  cdlemg33  40700  cdlemh  40806  cdlemk7u-2N  40877  cdlemk11u-2N  40878  cdlemk12u-2N  40879  cdlemk20-2N  40881  cdlemk28-3  40897  cdlemk33N  40898  cdlemk34  40899  cdlemk39  40905  cdlemkyyN  40951