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  29494  lshpkrlem5  40139  lplnexllnN  40589  4atexlemutvt  41079  cdlemc5  41220  cdlemd2  41224  cdleme0moN  41250  cdleme3h  41260  cdleme5  41265  cdleme9  41278  cdleme11l  41294  cdleme14  41298  cdleme15c  41301  cdleme16b  41304  cdleme16d  41306  cdleme16e  41307  cdlemednpq  41324  cdleme20bN  41335  cdleme20j  41343  cdleme20l2  41346  cdleme20l  41347  cdleme22cN  41367  cdleme22d  41368  cdleme22e  41369  cdleme22f  41371  cdleme26fALTN  41387  cdleme26f  41388  cdleme26f2ALTN  41389  cdleme26f2  41390  cdleme27a  41392  cdleme32b  41467  cdleme32d  41469  cdleme32f  41471  cdleme39n  41491  cdleme40n  41493  cdlemg2fv2  41625  cdlemg17h  41693  cdlemg27b  41721  cdlemg28b  41728  cdlemg28  41729  cdlemg29  41730  cdlemg33a  41731  cdlemg33d  41734  cdlemk7u-2N  41913  cdlemk11u-2N  41914  cdlemk12u-2N  41915  cdlemk26-3  41931  cdlemk27-3  41932  cdlemkfid3N  41950  cdlemn11c  42234