Theorem simp23l 1313

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

Assertion

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

Proof of Theorem simp23l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ax5seglem6  29399  lshpkrlem5  39995  lplnexllnN  40445  4atexlemt  40934  4atex2  40958  4atex3  40962  trlval4  41069  cdlemc5  41076  cdlemc6  41077  cdlemd2  41080  cdleme0e  41098  cdleme0moN  41106  cdleme3g  41115  cdleme3h  41116  cdleme3  41118  cdleme4  41119  cdleme5  41121  cdleme9  41134  cdleme11fN  41145  cdleme11j  41148  cdleme11k  41149  cdleme11l  41150  cdleme11  41151  cdleme14  41154  cdleme15a  41155  cdleme15b  41156  cdleme15c  41157  cdleme16b  41160  cdleme16c  41161  cdleme16d  41162  cdleme16e  41163  cdleme16f  41164  cdleme17d1  41170  cdleme18c  41174  cdlemednpq  41180  cdleme19c  41186  cdleme20bN  41191  cdleme20d  41193  cdleme20f  41195  cdleme20g  41196  cdleme20h  41197  cdleme20j  41199  cdleme20l2  41202  cdleme20l  41203  cdleme20m  41204  cdleme22cN  41223  cdleme22d  41224  cdleme22e  41225  cdleme22f  41227  cdleme26fALTN  41243  cdleme26f  41244  cdleme26f2ALTN  41245  cdleme26f2  41246  cdleme27a  41248  cdleme28a  41251  cdlemefs44  41307  cdlemefs45ee  41311  cdleme32b  41323  cdleme32c  41324  cdleme32e  41326  cdleme35sn2aw  41339  cdleme37m  41343  cdleme39n  41347  cdleme40n  41349  cdleme40w  41351  cdleme42k  41365  cdlemeg47rv2  41391  cdlemeg46rjgN  41403  cdlemeg46rgv  41409  cdlemeg46req  41410  cdlemg2fv2  41481  cdlemg17h  41549  cdlemg31b0a  41576  cdlemg27b  41577  cdlemg31d  41581  cdlemg28b  41584  cdlemg28  41585  cdlemg29  41586  cdlemg33a  41587  cdlemg33b  41588  cdlemg33c  41589  cdlemg33d  41590  cdlemg33e  41591  cdlemg44a  41612  cdlemk7u-2N  41769  cdlemk11u-2N  41770  cdlemk12u-2N  41771  cdlemk26-3  41787  cdlemk27-3  41788  cdlemkfid3N  41806  cdlemn2  42076  cdlemn10  42087  cdlemn11c  42090