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  28868  lshpkrlem5  39114  lplnexllnN  39565  4atexlemutvt  40055  cdlemc5  40196  cdlemd2  40200  cdleme0moN  40226  cdleme3h  40236  cdleme5  40241  cdleme9  40254  cdleme11l  40270  cdleme14  40274  cdleme15c  40277  cdleme16b  40280  cdleme16d  40282  cdleme16e  40283  cdlemednpq  40300  cdleme20bN  40311  cdleme20j  40319  cdleme20l2  40322  cdleme20l  40323  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22f  40347  cdleme26fALTN  40363  cdleme26f  40364  cdleme26f2ALTN  40365  cdleme26f2  40366  cdleme27a  40368  cdleme32b  40443  cdleme32d  40445  cdleme32f  40447  cdleme39n  40467  cdleme40n  40469  cdlemg2fv2  40601  cdlemg17h  40669  cdlemg27b  40697  cdlemg28b  40704  cdlemg28  40705  cdlemg29  40706  cdlemg33a  40707  cdlemg33d  40710  cdlemk7u-2N  40889  cdlemk11u-2N  40890  cdlemk12u-2N  40891  cdlemk26-3  40907  cdlemk27-3  40908  cdlemkfid3N  40926  cdlemn11c  41210