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  26723  lshpkrlem5  36254  lplnexllnN  36704  4atexlemutvt  37194  cdlemc5  37335  cdlemd2  37339  cdleme0moN  37365  cdleme3h  37375  cdleme5  37380  cdleme9  37393  cdleme11l  37409  cdleme14  37413  cdleme15c  37416  cdleme16b  37419  cdleme16d  37421  cdleme16e  37422  cdlemednpq  37439  cdleme20bN  37450  cdleme20j  37458  cdleme20l2  37461  cdleme20l  37462  cdleme22cN  37482  cdleme22d  37483  cdleme22e  37484  cdleme22f  37486  cdleme26fALTN  37502  cdleme26f  37503  cdleme26f2ALTN  37504  cdleme26f2  37505  cdleme27a  37507  cdleme32b  37582  cdleme32d  37584  cdleme32f  37586  cdleme39n  37606  cdleme40n  37608  cdlemg2fv2  37740  cdlemg17h  37808  cdlemg27b  37836  cdlemg28b  37843  cdlemg28  37844  cdlemg29  37845  cdlemg33a  37846  cdlemg33d  37849  cdlemk7u-2N  38028  cdlemk11u-2N  38029  cdlemk12u-2N  38030  cdlemk26-3  38046  cdlemk27-3  38047  cdlemkfid3N  38065  cdlemn11c  38349