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  39370  lplnexllnN  39820  4atexlemutvt  40310  cdlemc5  40451  cdlemd2  40455  cdleme0moN  40481  cdleme3h  40491  cdleme5  40496  cdleme9  40509  cdleme11l  40525  cdleme14  40529  cdleme15c  40532  cdleme16b  40535  cdleme16d  40537  cdleme16e  40538  cdlemednpq  40555  cdleme20bN  40566  cdleme20j  40574  cdleme20l2  40577  cdleme20l  40578  cdleme22cN  40598  cdleme22d  40599  cdleme22e  40600  cdleme22f  40602  cdleme26fALTN  40618  cdleme26f  40619  cdleme26f2ALTN  40620  cdleme26f2  40621  cdleme27a  40623  cdleme32b  40698  cdleme32d  40700  cdleme32f  40702  cdleme39n  40722  cdleme40n  40724  cdlemg2fv2  40856  cdlemg17h  40924  cdlemg27b  40952  cdlemg28b  40959  cdlemg28  40960  cdlemg29  40961  cdlemg33a  40962  cdlemg33d  40965  cdlemk7u-2N  41144  cdlemk11u-2N  41145  cdlemk12u-2N  41146  cdlemk26-3  41162  cdlemk27-3  41163  cdlemkfid3N  41181  cdlemn11c  41465