Theorem simp23r 1297

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

Assertion

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

Proof of Theorem simp23r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  ax5seglem6  29019  lshpkrlem5  39484  lplnexllnN  39934  4atexlemutvt  40424  cdlemc5  40565  cdlemd2  40569  cdleme0moN  40595  cdleme3h  40605  cdleme5  40610  cdleme9  40623  cdleme11l  40639  cdleme14  40643  cdleme15c  40646  cdleme16b  40649  cdleme16d  40651  cdleme16e  40652  cdlemednpq  40669  cdleme20bN  40680  cdleme20j  40688  cdleme20l2  40691  cdleme20l  40692  cdleme22cN  40712  cdleme22d  40713  cdleme22e  40714  cdleme22f  40716  cdleme26fALTN  40732  cdleme26f  40733  cdleme26f2ALTN  40734  cdleme26f2  40735  cdleme27a  40737  cdleme32b  40812  cdleme32d  40814  cdleme32f  40816  cdleme39n  40836  cdleme40n  40838  cdlemg2fv2  40970  cdlemg17h  41038  cdlemg27b  41066  cdlemg28b  41073  cdlemg28  41074  cdlemg29  41075  cdlemg33a  41076  cdlemg33d  41079  cdlemk7u-2N  41258  cdlemk11u-2N  41259  cdlemk12u-2N  41260  cdlemk26-3  41276  cdlemk27-3  41277  cdlemkfid3N  41295  cdlemn11c  41579