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  29321  lshpkrlem5  39929  lplnexllnN  40379  4atexlemutvt  40869  cdlemc5  41010  cdlemd2  41014  cdleme0moN  41040  cdleme3h  41050  cdleme5  41055  cdleme9  41068  cdleme11l  41084  cdleme14  41088  cdleme15c  41091  cdleme16b  41094  cdleme16d  41096  cdleme16e  41097  cdlemednpq  41114  cdleme20bN  41125  cdleme20j  41133  cdleme20l2  41136  cdleme20l  41137  cdleme22cN  41157  cdleme22d  41158  cdleme22e  41159  cdleme22f  41161  cdleme26fALTN  41177  cdleme26f  41178  cdleme26f2ALTN  41179  cdleme26f2  41180  cdleme27a  41182  cdleme32b  41257  cdleme32d  41259  cdleme32f  41261  cdleme39n  41281  cdleme40n  41283  cdlemg2fv2  41415  cdlemg17h  41483  cdlemg27b  41511  cdlemg28b  41518  cdlemg28  41519  cdlemg29  41520  cdlemg33a  41521  cdlemg33d  41524  cdlemk7u-2N  41703  cdlemk11u-2N  41704  cdlemk12u-2N  41705  cdlemk26-3  41721  cdlemk27-3  41722  cdlemkfid3N  41740  cdlemn11c  42024