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  28868  lshpkrlem5  39114  lplnexllnN  39565  4atexlemt  40054  4atex2  40078  4atex3  40082  trlval4  40189  cdlemc5  40196  cdlemc6  40197  cdlemd2  40200  cdleme0e  40218  cdleme0moN  40226  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme4  40239  cdleme5  40241  cdleme9  40254  cdleme11fN  40265  cdleme11j  40268  cdleme11k  40269  cdleme11l  40270  cdleme11  40271  cdleme14  40274  cdleme15a  40275  cdleme15b  40276  cdleme15c  40277  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme16e  40283  cdleme16f  40284  cdleme17d1  40290  cdleme18c  40294  cdlemednpq  40300  cdleme19c  40306  cdleme20bN  40311  cdleme20d  40313  cdleme20f  40315  cdleme20g  40316  cdleme20h  40317  cdleme20j  40319  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22f  40347  cdleme26fALTN  40363  cdleme26f  40364  cdleme26f2ALTN  40365  cdleme26f2  40366  cdleme27a  40368  cdleme28a  40371  cdlemefs44  40427  cdlemefs45ee  40431  cdleme32b  40443  cdleme32c  40444  cdleme32e  40446  cdleme35sn2aw  40459  cdleme37m  40463  cdleme39n  40467  cdleme40n  40469  cdleme40w  40471  cdleme42k  40485  cdlemeg47rv2  40511  cdlemeg46rjgN  40523  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemg2fv2  40601  cdlemg17h  40669  cdlemg31b0a  40696  cdlemg27b  40697  cdlemg31d  40701  cdlemg28b  40704  cdlemg28  40705  cdlemg29  40706  cdlemg33a  40707  cdlemg33b  40708  cdlemg33c  40709  cdlemg33d  40710  cdlemg33e  40711  cdlemg44a  40732  cdlemk7u-2N  40889  cdlemk11u-2N  40890  cdlemk12u-2N  40891  cdlemk26-3  40907  cdlemk27-3  40908  cdlemkfid3N  40926  cdlemn2  41196  cdlemn10  41207  cdlemn11c  41210