Theorem simp23l 1295

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

Assertion

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

Proof of Theorem simp23l

Step	Hyp	Ref	Expression
1		simp3l 1202	. 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  29007  lshpkrlem5  39370  lplnexllnN  39820  4atexlemt  40309  4atex2  40333  4atex3  40337  trlval4  40444  cdlemc5  40451  cdlemc6  40452  cdlemd2  40455  cdleme0e  40473  cdleme0moN  40481  cdleme3g  40490  cdleme3h  40491  cdleme3  40493  cdleme4  40494  cdleme5  40496  cdleme9  40509  cdleme11fN  40520  cdleme11j  40523  cdleme11k  40524  cdleme11l  40525  cdleme11  40526  cdleme14  40529  cdleme15a  40530  cdleme15b  40531  cdleme15c  40532  cdleme16b  40535  cdleme16c  40536  cdleme16d  40537  cdleme16e  40538  cdleme16f  40539  cdleme17d1  40545  cdleme18c  40549  cdlemednpq  40555  cdleme19c  40561  cdleme20bN  40566  cdleme20d  40568  cdleme20f  40570  cdleme20g  40571  cdleme20h  40572  cdleme20j  40574  cdleme20l2  40577  cdleme20l  40578  cdleme20m  40579  cdleme22cN  40598  cdleme22d  40599  cdleme22e  40600  cdleme22f  40602  cdleme26fALTN  40618  cdleme26f  40619  cdleme26f2ALTN  40620  cdleme26f2  40621  cdleme27a  40623  cdleme28a  40626  cdlemefs44  40682  cdlemefs45ee  40686  cdleme32b  40698  cdleme32c  40699  cdleme32e  40701  cdleme35sn2aw  40714  cdleme37m  40718  cdleme39n  40722  cdleme40n  40724  cdleme40w  40726  cdleme42k  40740  cdlemeg47rv2  40766  cdlemeg46rjgN  40778  cdlemeg46rgv  40784  cdlemeg46req  40785  cdlemg2fv2  40856  cdlemg17h  40924  cdlemg31b0a  40951  cdlemg27b  40952  cdlemg31d  40956  cdlemg28b  40959  cdlemg28  40960  cdlemg29  40961  cdlemg33a  40962  cdlemg33b  40963  cdlemg33c  40964  cdlemg33d  40965  cdlemg33e  40966  cdlemg44a  40987  cdlemk7u-2N  41144  cdlemk11u-2N  41145  cdlemk12u-2N  41146  cdlemk26-3  41162  cdlemk27-3  41163  cdlemkfid3N  41181  cdlemn2  41451  cdlemn10  41462  cdlemn11c  41465