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 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ax5seglem6  29262  lshpkrlem5  39866  lplnexllnN  40316  4atexlemutvt  40806  cdlemc5  40947  cdlemd2  40951  cdleme0moN  40977  cdleme3h  40987  cdleme5  40992  cdleme9  41005  cdleme11l  41021  cdleme14  41025  cdleme15c  41028  cdleme16b  41031  cdleme16d  41033  cdleme16e  41034  cdlemednpq  41051  cdleme20bN  41062  cdleme20j  41070  cdleme20l2  41073  cdleme20l  41074  cdleme22cN  41094  cdleme22d  41095  cdleme22e  41096  cdleme22f  41098  cdleme26fALTN  41114  cdleme26f  41115  cdleme26f2ALTN  41116  cdleme26f2  41117  cdleme27a  41119  cdleme32b  41194  cdleme32d  41196  cdleme32f  41198  cdleme39n  41218  cdleme40n  41220  cdlemg2fv2  41352  cdlemg17h  41420  cdlemg27b  41448  cdlemg28b  41455  cdlemg28  41456  cdlemg29  41457  cdlemg33a  41458  cdlemg33d  41461  cdlemk7u-2N  41640  cdlemk11u-2N  41641  cdlemk12u-2N  41642  cdlemk26-3  41658  cdlemk27-3  41659  cdlemkfid3N  41677  cdlemn11c  41961