Theorem simp23l 1293

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

Assertion

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

Proof of Theorem simp23l

Step	Hyp	Ref	Expression
1		simp3l 1200	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant2 1133	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ax5seglem6  27311  lshpkrlem5  37135  lplnexllnN  37585  4atexlemt  38074  4atex2  38098  4atex3  38102  trlval4  38209  cdlemc5  38216  cdlemc6  38217  cdlemd2  38220  cdleme0e  38238  cdleme0moN  38246  cdleme3g  38255  cdleme3h  38256  cdleme3  38258  cdleme4  38259  cdleme5  38261  cdleme9  38274  cdleme11fN  38285  cdleme11j  38288  cdleme11k  38289  cdleme11l  38290  cdleme11  38291  cdleme14  38294  cdleme15a  38295  cdleme15b  38296  cdleme15c  38297  cdleme16b  38300  cdleme16c  38301  cdleme16d  38302  cdleme16e  38303  cdleme16f  38304  cdleme17d1  38310  cdleme18c  38314  cdlemednpq  38320  cdleme19c  38326  cdleme20bN  38331  cdleme20d  38333  cdleme20f  38335  cdleme20g  38336  cdleme20h  38337  cdleme20j  38339  cdleme20l2  38342  cdleme20l  38343  cdleme20m  38344  cdleme22cN  38363  cdleme22d  38364  cdleme22e  38365  cdleme22f  38367  cdleme26fALTN  38383  cdleme26f  38384  cdleme26f2ALTN  38385  cdleme26f2  38386  cdleme27a  38388  cdleme28a  38391  cdlemefs44  38447  cdlemefs45ee  38451  cdleme32b  38463  cdleme32c  38464  cdleme32e  38466  cdleme35sn2aw  38479  cdleme37m  38483  cdleme39n  38487  cdleme40n  38489  cdleme40w  38491  cdleme42k  38505  cdlemeg47rv2  38531  cdlemeg46rjgN  38543  cdlemeg46rgv  38549  cdlemeg46req  38550  cdlemg2fv2  38621  cdlemg17h  38689  cdlemg31b0a  38716  cdlemg27b  38717  cdlemg31d  38721  cdlemg28b  38724  cdlemg28  38725  cdlemg29  38726  cdlemg33a  38727  cdlemg33b  38728  cdlemg33c  38729  cdlemg33d  38730  cdlemg33e  38731  cdlemg44a  38752  cdlemk7u-2N  38909  cdlemk11u-2N  38910  cdlemk12u-2N  38911  cdlemk26-3  38927  cdlemk27-3  38928  cdlemkfid3N  38946  cdlemn2  39216  cdlemn10  39227  cdlemn11c  39230