Theorem simp22r 1293

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

Assertion

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

Proof of Theorem simp22r

Step	Hyp	Ref	Expression
1		simp2r 1200	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1134	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  8336  ttrclselem2  9795  ax5seglem6  28967  segconeu  35975  3atlem2  39441  lplnexllnN  39521  lplncvrlvol2  39572  4atex  40033  cdleme3g  40191  cdleme3h  40192  cdleme11h  40223  cdleme20bN  40267  cdleme20c  40268  cdleme20f  40271  cdleme20g  40272  cdleme20j  40275  cdleme20l2  40278  cdleme20l  40279  cdleme21ct  40286  cdleme26e  40316  cdleme43fsv1snlem  40377  cdleme39n  40423  cdleme40m  40424  cdleme42k  40441  cdlemg6c  40577  cdlemg31d  40657  cdlemg33a  40663  cdlemg33c  40665  cdlemg33d  40666  cdlemg33e  40667  cdlemg33  40668  cdlemh  40774  cdlemk7u-2N  40845  cdlemk11u-2N  40846  cdlemk12u-2N  40847  cdlemk20-2N  40849  cdlemk28-3  40865  cdlemk33N  40866  cdlemk34  40867  cdlemk39  40873  cdlemkyyN  40919