Theorem simp22r 1312

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

Assertion

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

Proof of Theorem simp22r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  frrlem10  8297  ttrclselem2  9711  ax5seglem6  29494  segconeu  36746  3atlem2  40509  lplnexllnN  40589  lplncvrlvol2  40640  4atex  41101  cdleme3g  41259  cdleme3h  41260  cdleme11h  41291  cdleme20bN  41335  cdleme20c  41336  cdleme20f  41339  cdleme20g  41340  cdleme20j  41343  cdleme20l2  41346  cdleme20l  41347  cdleme21ct  41354  cdleme26e  41384  cdleme43fsv1snlem  41445  cdleme39n  41491  cdleme40m  41492  cdleme42k  41509  cdlemg6c  41645  cdlemg31d  41725  cdlemg33a  41731  cdlemg33c  41733  cdlemg33d  41734  cdlemg33e  41735  cdlemg33  41736  cdlemh  41842  cdlemk7u-2N  41913  cdlemk11u-2N  41914  cdlemk12u-2N  41915  cdlemk20-2N  41917  cdlemk28-3  41933  cdlemk33N  41934  cdlemk34  41935  cdlemk39  41941  cdlemkyyN  41987