Theorem simp23r 1294

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

Assertion

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

Proof of Theorem simp23r

Step	Hyp	Ref	Expression
1		simp3r 1201	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant2 1133	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  28964  lshpkrlem5  39096  lplnexllnN  39547  4atexlemutvt  40037  cdlemc5  40178  cdlemd2  40182  cdleme0moN  40208  cdleme3h  40218  cdleme5  40223  cdleme9  40236  cdleme11l  40252  cdleme14  40256  cdleme15c  40259  cdleme16b  40262  cdleme16d  40264  cdleme16e  40265  cdlemednpq  40282  cdleme20bN  40293  cdleme20j  40301  cdleme20l2  40304  cdleme20l  40305  cdleme22cN  40325  cdleme22d  40326  cdleme22e  40327  cdleme22f  40329  cdleme26fALTN  40345  cdleme26f  40346  cdleme26f2ALTN  40347  cdleme26f2  40348  cdleme27a  40350  cdleme32b  40425  cdleme32d  40427  cdleme32f  40429  cdleme39n  40449  cdleme40n  40451  cdlemg2fv2  40583  cdlemg17h  40651  cdlemg27b  40679  cdlemg28b  40686  cdlemg28  40687  cdlemg29  40688  cdlemg33a  40689  cdlemg33d  40692  cdlemk7u-2N  40871  cdlemk11u-2N  40872  cdlemk12u-2N  40873  cdlemk26-3  40889  cdlemk27-3  40890  cdlemkfid3N  40908  cdlemn11c  41192