Theorem simp22r 1310

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

Assertion

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

Proof of Theorem simp22r

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  frrlem10  8280  ttrclselem2  9683  ax5seglem6  29189  segconeu  36369  3atlem2  40115  lplnexllnN  40195  lplncvrlvol2  40246  4atex  40707  cdleme3g  40865  cdleme3h  40866  cdleme11h  40897  cdleme20bN  40941  cdleme20c  40942  cdleme20f  40945  cdleme20g  40946  cdleme20j  40949  cdleme20l2  40952  cdleme20l  40953  cdleme21ct  40960  cdleme26e  40990  cdleme43fsv1snlem  41051  cdleme39n  41097  cdleme40m  41098  cdleme42k  41115  cdlemg6c  41251  cdlemg31d  41331  cdlemg33a  41337  cdlemg33c  41339  cdlemg33d  41340  cdlemg33e  41341  cdlemg33  41342  cdlemh  41448  cdlemk7u-2N  41519  cdlemk11u-2N  41520  cdlemk12u-2N  41521  cdlemk20-2N  41523  cdlemk28-3  41539  cdlemk33N  41540  cdlemk34  41541  cdlemk39  41547  cdlemkyyN  41593