Theorem simp23l 1311

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ax5seglem6  29189  lshpkrlem5  39745  lplnexllnN  40195  4atexlemt  40684  4atex2  40708  4atex3  40712  trlval4  40819  cdlemc5  40826  cdlemc6  40827  cdlemd2  40830  cdleme0e  40848  cdleme0moN  40856  cdleme3g  40865  cdleme3h  40866  cdleme3  40868  cdleme4  40869  cdleme5  40871  cdleme9  40884  cdleme11fN  40895  cdleme11j  40898  cdleme11k  40899  cdleme11l  40900  cdleme11  40901  cdleme14  40904  cdleme15a  40905  cdleme15b  40906  cdleme15c  40907  cdleme16b  40910  cdleme16c  40911  cdleme16d  40912  cdleme16e  40913  cdleme16f  40914  cdleme17d1  40920  cdleme18c  40924  cdlemednpq  40930  cdleme19c  40936  cdleme20bN  40941  cdleme20d  40943  cdleme20f  40945  cdleme20g  40946  cdleme20h  40947  cdleme20j  40949  cdleme20l2  40952  cdleme20l  40953  cdleme20m  40954  cdleme22cN  40973  cdleme22d  40974  cdleme22e  40975  cdleme22f  40977  cdleme26fALTN  40993  cdleme26f  40994  cdleme26f2ALTN  40995  cdleme26f2  40996  cdleme27a  40998  cdleme28a  41001  cdlemefs44  41057  cdlemefs45ee  41061  cdleme32b  41073  cdleme32c  41074  cdleme32e  41076  cdleme35sn2aw  41089  cdleme37m  41093  cdleme39n  41097  cdleme40n  41099  cdleme40w  41101  cdleme42k  41115  cdlemeg47rv2  41141  cdlemeg46rjgN  41153  cdlemeg46rgv  41159  cdlemeg46req  41160  cdlemg2fv2  41231  cdlemg17h  41299  cdlemg31b0a  41326  cdlemg27b  41327  cdlemg31d  41331  cdlemg28b  41334  cdlemg28  41335  cdlemg29  41336  cdlemg33a  41337  cdlemg33b  41338  cdlemg33c  41339  cdlemg33d  41340  cdlemg33e  41341  cdlemg44a  41362  cdlemk7u-2N  41519  cdlemk11u-2N  41520  cdlemk12u-2N  41521  cdlemk26-3  41537  cdlemk27-3  41538  cdlemkfid3N  41556  cdlemn2  41826  cdlemn10  41837  cdlemn11c  41840