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  28897  lshpkrlem5  39092  lplnexllnN  39543  4atexlemutvt  40033  cdlemc5  40174  cdlemd2  40178  cdleme0moN  40204  cdleme3h  40214  cdleme5  40219  cdleme9  40232  cdleme11l  40248  cdleme14  40252  cdleme15c  40255  cdleme16b  40258  cdleme16d  40260  cdleme16e  40261  cdlemednpq  40278  cdleme20bN  40289  cdleme20j  40297  cdleme20l2  40300  cdleme20l  40301  cdleme22cN  40321  cdleme22d  40322  cdleme22e  40323  cdleme22f  40325  cdleme26fALTN  40341  cdleme26f  40342  cdleme26f2ALTN  40343  cdleme26f2  40344  cdleme27a  40346  cdleme32b  40421  cdleme32d  40423  cdleme32f  40425  cdleme39n  40445  cdleme40n  40447  cdlemg2fv2  40579  cdlemg17h  40647  cdlemg27b  40675  cdlemg28b  40682  cdlemg28  40683  cdlemg29  40684  cdlemg33a  40685  cdlemg33d  40688  cdlemk7u-2N  40867  cdlemk11u-2N  40868  cdlemk12u-2N  40869  cdlemk26-3  40885  cdlemk27-3  40886  cdlemkfid3N  40904  cdlemn11c  41188