Theorem simp23r 1296

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  ax5seglem6  28223  lshpkrlem5  38032  lplnexllnN  38483  4atexlemutvt  38973  cdlemc5  39114  cdlemd2  39118  cdleme0moN  39144  cdleme3h  39154  cdleme5  39159  cdleme9  39172  cdleme11l  39188  cdleme14  39192  cdleme15c  39195  cdleme16b  39198  cdleme16d  39200  cdleme16e  39201  cdlemednpq  39218  cdleme20bN  39229  cdleme20j  39237  cdleme20l2  39240  cdleme20l  39241  cdleme22cN  39261  cdleme22d  39262  cdleme22e  39263  cdleme22f  39265  cdleme26fALTN  39281  cdleme26f  39282  cdleme26f2ALTN  39283  cdleme26f2  39284  cdleme27a  39286  cdleme32b  39361  cdleme32d  39363  cdleme32f  39365  cdleme39n  39385  cdleme40n  39387  cdlemg2fv2  39519  cdlemg17h  39587  cdlemg27b  39615  cdlemg28b  39622  cdlemg28  39623  cdlemg29  39624  cdlemg33a  39625  cdlemg33d  39628  cdlemk7u-2N  39807  cdlemk11u-2N  39808  cdlemk12u-2N  39809  cdlemk26-3  39825  cdlemk27-3  39826  cdlemkfid3N  39844  cdlemn11c  40128