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  29007  lshpkrlem5  39374  lplnexllnN  39824  4atexlemutvt  40314  cdlemc5  40455  cdlemd2  40459  cdleme0moN  40485  cdleme3h  40495  cdleme5  40500  cdleme9  40513  cdleme11l  40529  cdleme14  40533  cdleme15c  40536  cdleme16b  40539  cdleme16d  40541  cdleme16e  40542  cdlemednpq  40559  cdleme20bN  40570  cdleme20j  40578  cdleme20l2  40581  cdleme20l  40582  cdleme22cN  40602  cdleme22d  40603  cdleme22e  40604  cdleme22f  40606  cdleme26fALTN  40622  cdleme26f  40623  cdleme26f2ALTN  40624  cdleme26f2  40625  cdleme27a  40627  cdleme32b  40702  cdleme32d  40704  cdleme32f  40706  cdleme39n  40726  cdleme40n  40728  cdlemg2fv2  40860  cdlemg17h  40928  cdlemg27b  40956  cdlemg28b  40963  cdlemg28  40964  cdlemg29  40965  cdlemg33a  40966  cdlemg33d  40969  cdlemk7u-2N  41148  cdlemk11u-2N  41149  cdlemk12u-2N  41150  cdlemk26-3  41166  cdlemk27-3  41167  cdlemkfid3N  41185  cdlemn11c  41469