Theorem simp23r 1308

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ax5seglem6  29081  lshpkrlem5  39702  lplnexllnN  40152  4atexlemutvt  40642  cdlemc5  40783  cdlemd2  40787  cdleme0moN  40813  cdleme3h  40823  cdleme5  40828  cdleme9  40841  cdleme11l  40857  cdleme14  40861  cdleme15c  40864  cdleme16b  40867  cdleme16d  40869  cdleme16e  40870  cdlemednpq  40887  cdleme20bN  40898  cdleme20j  40906  cdleme20l2  40909  cdleme20l  40910  cdleme22cN  40930  cdleme22d  40931  cdleme22e  40932  cdleme22f  40934  cdleme26fALTN  40950  cdleme26f  40951  cdleme26f2ALTN  40952  cdleme26f2  40953  cdleme27a  40955  cdleme32b  41030  cdleme32d  41032  cdleme32f  41034  cdleme39n  41054  cdleme40n  41056  cdlemg2fv2  41188  cdlemg17h  41256  cdlemg27b  41284  cdlemg28b  41291  cdlemg28  41292  cdlemg29  41293  cdlemg33a  41294  cdlemg33d  41297  cdlemk7u-2N  41476  cdlemk11u-2N  41477  cdlemk12u-2N  41478  cdlemk26-3  41494  cdlemk27-3  41495  cdlemkfid3N  41513  cdlemn11c  41797