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 1135	1 ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  ax5seglem6  28949  lshpkrlem5  39115  lplnexllnN  39566  4atexlemt  40055  4atex2  40079  4atex3  40083  trlval4  40190  cdlemc5  40197  cdlemc6  40198  cdlemd2  40201  cdleme0e  40219  cdleme0moN  40227  cdleme3g  40236  cdleme3h  40237  cdleme3  40239  cdleme4  40240  cdleme5  40242  cdleme9  40255  cdleme11fN  40266  cdleme11j  40269  cdleme11k  40270  cdleme11l  40271  cdleme11  40272  cdleme14  40275  cdleme15a  40276  cdleme15b  40277  cdleme15c  40278  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme16e  40284  cdleme16f  40285  cdleme17d1  40291  cdleme18c  40295  cdlemednpq  40301  cdleme19c  40307  cdleme20bN  40312  cdleme20d  40314  cdleme20f  40316  cdleme20g  40317  cdleme20h  40318  cdleme20j  40320  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22f  40348  cdleme26fALTN  40364  cdleme26f  40365  cdleme26f2ALTN  40366  cdleme26f2  40367  cdleme27a  40369  cdleme28a  40372  cdlemefs44  40428  cdlemefs45ee  40432  cdleme32b  40444  cdleme32c  40445  cdleme32e  40447  cdleme35sn2aw  40460  cdleme37m  40464  cdleme39n  40468  cdleme40n  40470  cdleme40w  40472  cdleme42k  40486  cdlemeg47rv2  40512  cdlemeg46rjgN  40524  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemg2fv2  40602  cdlemg17h  40670  cdlemg31b0a  40697  cdlemg27b  40698  cdlemg31d  40702  cdlemg28b  40705  cdlemg28  40706  cdlemg29  40707  cdlemg33a  40708  cdlemg33b  40709  cdlemg33c  40710  cdlemg33d  40711  cdlemg33e  40712  cdlemg44a  40733  cdlemk7u-2N  40890  cdlemk11u-2N  40891  cdlemk12u-2N  40892  cdlemk26-3  40908  cdlemk27-3  40909  cdlemkfid3N  40927  cdlemn2  41197  cdlemn10  41208  cdlemn11c  41211