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  28913  lshpkrlem5  39132  lplnexllnN  39583  4atexlemt  40072  4atex2  40096  4atex3  40100  trlval4  40207  cdlemc5  40214  cdlemc6  40215  cdlemd2  40218  cdleme0e  40236  cdleme0moN  40244  cdleme3g  40253  cdleme3h  40254  cdleme3  40256  cdleme4  40257  cdleme5  40259  cdleme9  40272  cdleme11fN  40283  cdleme11j  40286  cdleme11k  40287  cdleme11l  40288  cdleme11  40289  cdleme14  40292  cdleme15a  40293  cdleme15b  40294  cdleme15c  40295  cdleme16b  40298  cdleme16c  40299  cdleme16d  40300  cdleme16e  40301  cdleme16f  40302  cdleme17d1  40308  cdleme18c  40312  cdlemednpq  40318  cdleme19c  40324  cdleme20bN  40329  cdleme20d  40331  cdleme20f  40333  cdleme20g  40334  cdleme20h  40335  cdleme20j  40337  cdleme20l2  40340  cdleme20l  40341  cdleme20m  40342  cdleme22cN  40361  cdleme22d  40362  cdleme22e  40363  cdleme22f  40365  cdleme26fALTN  40381  cdleme26f  40382  cdleme26f2ALTN  40383  cdleme26f2  40384  cdleme27a  40386  cdleme28a  40389  cdlemefs44  40445  cdlemefs45ee  40449  cdleme32b  40461  cdleme32c  40462  cdleme32e  40464  cdleme35sn2aw  40477  cdleme37m  40481  cdleme39n  40485  cdleme40n  40487  cdleme40w  40489  cdleme42k  40503  cdlemeg47rv2  40529  cdlemeg46rjgN  40541  cdlemeg46rgv  40547  cdlemeg46req  40548  cdlemg2fv2  40619  cdlemg17h  40687  cdlemg31b0a  40714  cdlemg27b  40715  cdlemg31d  40719  cdlemg28b  40722  cdlemg28  40723  cdlemg29  40724  cdlemg33a  40725  cdlemg33b  40726  cdlemg33c  40727  cdlemg33d  40728  cdlemg33e  40729  cdlemg44a  40750  cdlemk7u-2N  40907  cdlemk11u-2N  40908  cdlemk12u-2N  40909  cdlemk26-3  40925  cdlemk27-3  40926  cdlemkfid3N  40944  cdlemn2  41214  cdlemn10  41225  cdlemn11c  41228