Theorem simp23r 1314

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

Assertion

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

Proof of Theorem simp23r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ax5seglem6  29517  lshpkrlem5  40264  lplnexllnN  40714  4atexlemutvt  41204  cdlemc5  41345  cdlemd2  41349  cdleme0moN  41375  cdleme3h  41385  cdleme5  41390  cdleme9  41403  cdleme11l  41419  cdleme14  41423  cdleme15c  41426  cdleme16b  41429  cdleme16d  41431  cdleme16e  41432  cdlemednpq  41449  cdleme20bN  41460  cdleme20j  41468  cdleme20l2  41471  cdleme20l  41472  cdleme22cN  41492  cdleme22d  41493  cdleme22e  41494  cdleme22f  41496  cdleme26fALTN  41512  cdleme26f  41513  cdleme26f2ALTN  41514  cdleme26f2  41515  cdleme27a  41517  cdleme32b  41592  cdleme32d  41594  cdleme32f  41596  cdleme39n  41616  cdleme40n  41618  cdlemg2fv2  41750  cdlemg17h  41818  cdlemg27b  41846  cdlemg28b  41853  cdlemg28  41854  cdlemg29  41855  cdlemg33a  41856  cdlemg33d  41859  cdlemk7u-2N  42038  cdlemk11u-2N  42039  cdlemk12u-2N  42040  cdlemk26-3  42056  cdlemk27-3  42057  cdlemkfid3N  42075  cdlemn11c  42359