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  28914  lshpkrlem5  39233  lplnexllnN  39683  4atexlemutvt  40173  cdlemc5  40314  cdlemd2  40318  cdleme0moN  40344  cdleme3h  40354  cdleme5  40359  cdleme9  40372  cdleme11l  40388  cdleme14  40392  cdleme15c  40395  cdleme16b  40398  cdleme16d  40400  cdleme16e  40401  cdlemednpq  40418  cdleme20bN  40429  cdleme20j  40437  cdleme20l2  40440  cdleme20l  40441  cdleme22cN  40461  cdleme22d  40462  cdleme22e  40463  cdleme22f  40465  cdleme26fALTN  40481  cdleme26f  40482  cdleme26f2ALTN  40483  cdleme26f2  40484  cdleme27a  40486  cdleme32b  40561  cdleme32d  40563  cdleme32f  40565  cdleme39n  40585  cdleme40n  40587  cdlemg2fv2  40719  cdlemg17h  40787  cdlemg27b  40815  cdlemg28b  40822  cdlemg28  40823  cdlemg29  40824  cdlemg33a  40825  cdlemg33d  40828  cdlemk7u-2N  41007  cdlemk11u-2N  41008  cdlemk12u-2N  41009  cdlemk26-3  41025  cdlemk27-3  41026  cdlemkfid3N  41044  cdlemn11c  41328