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  28861  lshpkrlem5  39107  lplnexllnN  39558  4atexlemutvt  40048  cdlemc5  40189  cdlemd2  40193  cdleme0moN  40219  cdleme3h  40229  cdleme5  40234  cdleme9  40247  cdleme11l  40263  cdleme14  40267  cdleme15c  40270  cdleme16b  40273  cdleme16d  40275  cdleme16e  40276  cdlemednpq  40293  cdleme20bN  40304  cdleme20j  40312  cdleme20l2  40315  cdleme20l  40316  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22f  40340  cdleme26fALTN  40356  cdleme26f  40357  cdleme26f2ALTN  40358  cdleme26f2  40359  cdleme27a  40361  cdleme32b  40436  cdleme32d  40438  cdleme32f  40440  cdleme39n  40460  cdleme40n  40462  cdlemg2fv2  40594  cdlemg17h  40662  cdlemg27b  40690  cdlemg28b  40697  cdlemg28  40698  cdlemg29  40699  cdlemg33a  40700  cdlemg33d  40703  cdlemk7u-2N  40882  cdlemk11u-2N  40883  cdlemk12u-2N  40884  cdlemk26-3  40900  cdlemk27-3  40901  cdlemkfid3N  40919  cdlemn11c  41203