Theorem simp23r 1292

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  ax5seglem6  28910  lshpkrlem5  38897  lplnexllnN  39348  4atexlemutvt  39838  cdlemc5  39979  cdlemd2  39983  cdleme0moN  40009  cdleme3h  40019  cdleme5  40024  cdleme9  40037  cdleme11l  40053  cdleme14  40057  cdleme15c  40060  cdleme16b  40063  cdleme16d  40065  cdleme16e  40066  cdlemednpq  40083  cdleme20bN  40094  cdleme20j  40102  cdleme20l2  40105  cdleme20l  40106  cdleme22cN  40126  cdleme22d  40127  cdleme22e  40128  cdleme22f  40130  cdleme26fALTN  40146  cdleme26f  40147  cdleme26f2ALTN  40148  cdleme26f2  40149  cdleme27a  40151  cdleme32b  40226  cdleme32d  40228  cdleme32f  40230  cdleme39n  40250  cdleme40n  40252  cdlemg2fv2  40384  cdlemg17h  40452  cdlemg27b  40480  cdlemg28b  40487  cdlemg28  40488  cdlemg29  40489  cdlemg33a  40490  cdlemg33d  40493  cdlemk7u-2N  40672  cdlemk11u-2N  40673  cdlemk12u-2N  40674  cdlemk26-3  40690  cdlemk27-3  40691  cdlemkfid3N  40709  cdlemn11c  40993