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  28910  lshpkrlem5  39152  lplnexllnN  39602  4atexlemutvt  40092  cdlemc5  40233  cdlemd2  40237  cdleme0moN  40263  cdleme3h  40273  cdleme5  40278  cdleme9  40291  cdleme11l  40307  cdleme14  40311  cdleme15c  40314  cdleme16b  40317  cdleme16d  40319  cdleme16e  40320  cdlemednpq  40337  cdleme20bN  40348  cdleme20j  40356  cdleme20l2  40359  cdleme20l  40360  cdleme22cN  40380  cdleme22d  40381  cdleme22e  40382  cdleme22f  40384  cdleme26fALTN  40400  cdleme26f  40401  cdleme26f2ALTN  40402  cdleme26f2  40403  cdleme27a  40405  cdleme32b  40480  cdleme32d  40482  cdleme32f  40484  cdleme39n  40504  cdleme40n  40506  cdlemg2fv2  40638  cdlemg17h  40706  cdlemg27b  40734  cdlemg28b  40741  cdlemg28  40742  cdlemg29  40743  cdlemg33a  40744  cdlemg33d  40747  cdlemk7u-2N  40926  cdlemk11u-2N  40927  cdlemk12u-2N  40928  cdlemk26-3  40944  cdlemk27-3  40945  cdlemkfid3N  40963  cdlemn11c  41247