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 1135	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  frrlem10  8320  ttrclselem2  9766  ax5seglem6  28949  segconeu  36012  3atlem2  39486  lplnexllnN  39566  lplncvrlvol2  39617  4atex  40078  cdleme3g  40236  cdleme3h  40237  cdleme11h  40268  cdleme20bN  40312  cdleme20c  40313  cdleme20f  40316  cdleme20g  40317  cdleme20j  40320  cdleme20l2  40323  cdleme20l  40324  cdleme21ct  40331  cdleme26e  40361  cdleme43fsv1snlem  40422  cdleme39n  40468  cdleme40m  40469  cdleme42k  40486  cdlemg6c  40622  cdlemg31d  40702  cdlemg33a  40708  cdlemg33c  40710  cdlemg33d  40711  cdlemg33e  40712  cdlemg33  40713  cdlemh  40819  cdlemk7u-2N  40890  cdlemk11u-2N  40891  cdlemk12u-2N  40892  cdlemk20-2N  40894  cdlemk28-3  40910  cdlemk33N  40911  cdlemk34  40912  cdlemk39  40918  cdlemkyyN  40964