Theorem simp22r 1295

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

Assertion

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

Proof of Theorem simp22r

Step	Hyp	Ref	Expression
1		simp2r 1202	. 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  8238  ttrclselem2  9638  ax5seglem6  29017  segconeu  36209  3atlem2  39944  lplnexllnN  40024  lplncvrlvol2  40075  4atex  40536  cdleme3g  40694  cdleme3h  40695  cdleme11h  40726  cdleme20bN  40770  cdleme20c  40771  cdleme20f  40774  cdleme20g  40775  cdleme20j  40778  cdleme20l2  40781  cdleme20l  40782  cdleme21ct  40789  cdleme26e  40819  cdleme43fsv1snlem  40880  cdleme39n  40926  cdleme40m  40927  cdleme42k  40944  cdlemg6c  41080  cdlemg31d  41160  cdlemg33a  41166  cdlemg33c  41168  cdlemg33d  41169  cdlemg33e  41170  cdlemg33  41171  cdlemh  41277  cdlemk7u-2N  41348  cdlemk11u-2N  41349  cdlemk12u-2N  41350  cdlemk20-2N  41352  cdlemk28-3  41368  cdlemk33N  41369  cdlemk34  41370  cdlemk39  41376  cdlemkyyN  41422