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  8235  ttrclselem2  9641  ax5seglem6  28897  segconeu  35987  3atlem2  39466  lplnexllnN  39546  lplncvrlvol2  39597  4atex  40058  cdleme3g  40216  cdleme3h  40217  cdleme11h  40248  cdleme20bN  40292  cdleme20c  40293  cdleme20f  40296  cdleme20g  40297  cdleme20j  40300  cdleme20l2  40303  cdleme20l  40304  cdleme21ct  40311  cdleme26e  40341  cdleme43fsv1snlem  40402  cdleme39n  40448  cdleme40m  40449  cdleme42k  40466  cdlemg6c  40602  cdlemg31d  40682  cdlemg33a  40688  cdlemg33c  40690  cdlemg33d  40691  cdlemg33e  40692  cdlemg33  40693  cdlemh  40799  cdlemk7u-2N  40870  cdlemk11u-2N  40871  cdlemk12u-2N  40872  cdlemk20-2N  40874  cdlemk28-3  40890  cdlemk33N  40891  cdlemk34  40892  cdlemk39  40898  cdlemkyyN  40944