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  29545  lshpkrlem5  40374  lplnexllnN  40824  4atexlemt  41313  4atex2  41337  4atex3  41341  trlval4  41448  cdlemc5  41455  cdlemc6  41456  cdlemd2  41459  cdleme0e  41477  cdleme0moN  41485  cdleme3g  41494  cdleme3h  41495  cdleme3  41497  cdleme4  41498  cdleme5  41500  cdleme9  41513  cdleme11fN  41524  cdleme11j  41527  cdleme11k  41528  cdleme11l  41529  cdleme11  41530  cdleme14  41533  cdleme15a  41534  cdleme15b  41535  cdleme15c  41536  cdleme16b  41539  cdleme16c  41540  cdleme16d  41541  cdleme16e  41542  cdleme16f  41543  cdleme17d1  41549  cdleme18c  41553  cdlemednpq  41559  cdleme19c  41565  cdleme20bN  41570  cdleme20d  41572  cdleme20f  41574  cdleme20g  41575  cdleme20h  41576  cdleme20j  41578  cdleme20l2  41581  cdleme20l  41582  cdleme20m  41583  cdleme22cN  41602  cdleme22d  41603  cdleme22e  41604  cdleme22f  41606  cdleme26fALTN  41622  cdleme26f  41623  cdleme26f2ALTN  41624  cdleme26f2  41625  cdleme27a  41627  cdleme28a  41630  cdlemefs44  41686  cdlemefs45ee  41690  cdleme32b  41702  cdleme32c  41703  cdleme32e  41705  cdleme35sn2aw  41718  cdleme37m  41722  cdleme39n  41726  cdleme40n  41728  cdleme40w  41730  cdleme42k  41744  cdlemeg47rv2  41770  cdlemeg46rjgN  41782  cdlemeg46rgv  41788  cdlemeg46req  41789  cdlemg2fv2  41860  cdlemg17h  41928  cdlemg31b0a  41955  cdlemg27b  41956  cdlemg31d  41960  cdlemg28b  41963  cdlemg28  41964  cdlemg29  41965  cdlemg33a  41966  cdlemg33b  41967  cdlemg33c  41968  cdlemg33d  41969  cdlemg33e  41970  cdlemg44a  41991  cdlemk7u-2N  42148  cdlemk11u-2N  42149  cdlemk12u-2N  42150  cdlemk26-3  42166  cdlemk27-3  42167  cdlemkfid3N  42185  cdlemn2  42455  cdlemn10  42466  cdlemn11c  42469