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 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:  ax5seglem6  28913  lshpkrlem5  39132  lplnexllnN  39583  4atexlemutvt  40073  cdlemc5  40214  cdlemd2  40218  cdleme0moN  40244  cdleme3h  40254  cdleme5  40259  cdleme9  40272  cdleme11l  40288  cdleme14  40292  cdleme15c  40295  cdleme16b  40298  cdleme16d  40300  cdleme16e  40301  cdlemednpq  40318  cdleme20bN  40329  cdleme20j  40337  cdleme20l2  40340  cdleme20l  40341  cdleme22cN  40361  cdleme22d  40362  cdleme22e  40363  cdleme22f  40365  cdleme26fALTN  40381  cdleme26f  40382  cdleme26f2ALTN  40383  cdleme26f2  40384  cdleme27a  40386  cdleme32b  40461  cdleme32d  40463  cdleme32f  40465  cdleme39n  40485  cdleme40n  40487  cdlemg2fv2  40619  cdlemg17h  40687  cdlemg27b  40715  cdlemg28b  40722  cdlemg28  40723  cdlemg29  40724  cdlemg33a  40725  cdlemg33d  40728  cdlemk7u-2N  40907  cdlemk11u-2N  40908  cdlemk12u-2N  40909  cdlemk26-3  40925  cdlemk27-3  40926  cdlemkfid3N  40944  cdlemn11c  41228