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 394   ∧ 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 206  df-an 395  df-3an 1086

This theorem is referenced by:  frrlem10  8301  ttrclselem2  9751  ax5seglem6  28817  segconeu  35735  3atlem2  39084  lplnexllnN  39164  lplncvrlvol2  39215  4atex  39676  cdleme3g  39834  cdleme3h  39835  cdleme11h  39866  cdleme20bN  39910  cdleme20c  39911  cdleme20f  39914  cdleme20g  39915  cdleme20j  39918  cdleme20l2  39921  cdleme20l  39922  cdleme21ct  39929  cdleme26e  39959  cdleme43fsv1snlem  40020  cdleme39n  40066  cdleme40m  40067  cdleme42k  40084  cdlemg6c  40220  cdlemg31d  40300  cdlemg33a  40306  cdlemg33c  40308  cdlemg33d  40309  cdlemg33e  40310  cdlemg33  40311  cdlemh  40417  cdlemk7u-2N  40488  cdlemk11u-2N  40489  cdlemk12u-2N  40490  cdlemk20-2N  40492  cdlemk28-3  40508  cdlemk33N  40509  cdlemk34  40510  cdlemk39  40516  cdlemkyyN  40562