Theorem simp23r 1314

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

Assertion

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

Proof of Theorem simp23r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ax5seglem6  29545  lshpkrlem5  40374  lplnexllnN  40824  4atexlemutvt  41314  cdlemc5  41455  cdlemd2  41459  cdleme0moN  41485  cdleme3h  41495  cdleme5  41500  cdleme9  41513  cdleme11l  41529  cdleme14  41533  cdleme15c  41536  cdleme16b  41539  cdleme16d  41541  cdleme16e  41542  cdlemednpq  41559  cdleme20bN  41570  cdleme20j  41578  cdleme20l2  41581  cdleme20l  41582  cdleme22cN  41602  cdleme22d  41603  cdleme22e  41604  cdleme22f  41606  cdleme26fALTN  41622  cdleme26f  41623  cdleme26f2ALTN  41624  cdleme26f2  41625  cdleme27a  41627  cdleme32b  41702  cdleme32d  41704  cdleme32f  41706  cdleme39n  41726  cdleme40n  41728  cdlemg2fv2  41860  cdlemg17h  41928  cdlemg27b  41956  cdlemg28b  41963  cdlemg28  41964  cdlemg29  41965  cdlemg33a  41966  cdlemg33d  41969  cdlemk7u-2N  42148  cdlemk11u-2N  42149  cdlemk12u-2N  42150  cdlemk26-3  42166  cdlemk27-3  42167  cdlemkfid3N  42185  cdlemn11c  42469