Theorem simp23r 1295

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

Assertion

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

Proof of Theorem simp23r

Step	Hyp	Ref	Expression
1		simp3r 1202	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant2 1134	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  ax5seglem6  28057  lshpkrlem5  37787  lplnexllnN  38238  4atexlemutvt  38728  cdlemc5  38869  cdlemd2  38873  cdleme0moN  38899  cdleme3h  38909  cdleme5  38914  cdleme9  38927  cdleme11l  38943  cdleme14  38947  cdleme15c  38950  cdleme16b  38953  cdleme16d  38955  cdleme16e  38956  cdlemednpq  38973  cdleme20bN  38984  cdleme20j  38992  cdleme20l2  38995  cdleme20l  38996  cdleme22cN  39016  cdleme22d  39017  cdleme22e  39018  cdleme22f  39020  cdleme26fALTN  39036  cdleme26f  39037  cdleme26f2ALTN  39038  cdleme26f2  39039  cdleme27a  39041  cdleme32b  39116  cdleme32d  39118  cdleme32f  39120  cdleme39n  39140  cdleme40n  39142  cdlemg2fv2  39274  cdlemg17h  39342  cdlemg27b  39370  cdlemg28b  39377  cdlemg28  39378  cdlemg29  39379  cdlemg33a  39380  cdlemg33d  39383  cdlemk7u-2N  39562  cdlemk11u-2N  39563  cdlemk12u-2N  39564  cdlemk26-3  39580  cdlemk27-3  39581  cdlemkfid3N  39599  cdlemn11c  39883