Theorem simp23l 1296

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

Assertion

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

Proof of Theorem simp23l

Step	Hyp	Ref	Expression
1		simp3l 1203	. 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  29019  lshpkrlem5  39484  lplnexllnN  39934  4atexlemt  40423  4atex2  40447  4atex3  40451  trlval4  40558  cdlemc5  40565  cdlemc6  40566  cdlemd2  40569  cdleme0e  40587  cdleme0moN  40595  cdleme3g  40604  cdleme3h  40605  cdleme3  40607  cdleme4  40608  cdleme5  40610  cdleme9  40623  cdleme11fN  40634  cdleme11j  40637  cdleme11k  40638  cdleme11l  40639  cdleme11  40640  cdleme14  40643  cdleme15a  40644  cdleme15b  40645  cdleme15c  40646  cdleme16b  40649  cdleme16c  40650  cdleme16d  40651  cdleme16e  40652  cdleme16f  40653  cdleme17d1  40659  cdleme18c  40663  cdlemednpq  40669  cdleme19c  40675  cdleme20bN  40680  cdleme20d  40682  cdleme20f  40684  cdleme20g  40685  cdleme20h  40686  cdleme20j  40688  cdleme20l2  40691  cdleme20l  40692  cdleme20m  40693  cdleme22cN  40712  cdleme22d  40713  cdleme22e  40714  cdleme22f  40716  cdleme26fALTN  40732  cdleme26f  40733  cdleme26f2ALTN  40734  cdleme26f2  40735  cdleme27a  40737  cdleme28a  40740  cdlemefs44  40796  cdlemefs45ee  40800  cdleme32b  40812  cdleme32c  40813  cdleme32e  40815  cdleme35sn2aw  40828  cdleme37m  40832  cdleme39n  40836  cdleme40n  40838  cdleme40w  40840  cdleme42k  40854  cdlemeg47rv2  40880  cdlemeg46rjgN  40892  cdlemeg46rgv  40898  cdlemeg46req  40899  cdlemg2fv2  40970  cdlemg17h  41038  cdlemg31b0a  41065  cdlemg27b  41066  cdlemg31d  41070  cdlemg28b  41073  cdlemg28  41074  cdlemg29  41075  cdlemg33a  41076  cdlemg33b  41077  cdlemg33c  41078  cdlemg33d  41079  cdlemg33e  41080  cdlemg44a  41101  cdlemk7u-2N  41258  cdlemk11u-2N  41259  cdlemk12u-2N  41260  cdlemk26-3  41276  cdlemk27-3  41277  cdlemkfid3N  41295  cdlemn2  41565  cdlemn10  41576  cdlemn11c  41579