Theorem simp23r 1291

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ax5seglem6  26714  lshpkrlem5  36244  lplnexllnN  36694  4atexlemutvt  37184  cdlemc5  37325  cdlemd2  37329  cdleme0moN  37355  cdleme3h  37365  cdleme5  37370  cdleme9  37383  cdleme11l  37399  cdleme14  37403  cdleme15c  37406  cdleme16b  37409  cdleme16d  37411  cdleme16e  37412  cdlemednpq  37429  cdleme20bN  37440  cdleme20j  37448  cdleme20l2  37451  cdleme20l  37452  cdleme22cN  37472  cdleme22d  37473  cdleme22e  37474  cdleme22f  37476  cdleme26fALTN  37492  cdleme26f  37493  cdleme26f2ALTN  37494  cdleme26f2  37495  cdleme27a  37497  cdleme32b  37572  cdleme32d  37574  cdleme32f  37576  cdleme39n  37596  cdleme40n  37598  cdlemg2fv2  37730  cdlemg17h  37798  cdlemg27b  37826  cdlemg28b  37833  cdlemg28  37834  cdlemg29  37835  cdlemg33a  37836  cdlemg33d  37839  cdlemk7u-2N  38018  cdlemk11u-2N  38019  cdlemk12u-2N  38020  cdlemk26-3  38036  cdlemk27-3  38037  cdlemkfid3N  38055  cdlemn11c  38339