Theorem simp23l 1290

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ax5seglem6  26714  lshpkrlem5  36244  lplnexllnN  36694  4atexlemt  37183  4atex2  37207  4atex3  37211  trlval4  37318  cdlemc5  37325  cdlemc6  37326  cdlemd2  37329  cdleme0e  37347  cdleme0moN  37355  cdleme3g  37364  cdleme3h  37365  cdleme3  37367  cdleme4  37368  cdleme5  37370  cdleme9  37383  cdleme11fN  37394  cdleme11j  37397  cdleme11k  37398  cdleme11l  37399  cdleme11  37400  cdleme14  37403  cdleme15a  37404  cdleme15b  37405  cdleme15c  37406  cdleme16b  37409  cdleme16c  37410  cdleme16d  37411  cdleme16e  37412  cdleme16f  37413  cdleme17d1  37419  cdleme18c  37423  cdlemednpq  37429  cdleme19c  37435  cdleme20bN  37440  cdleme20d  37442  cdleme20f  37444  cdleme20g  37445  cdleme20h  37446  cdleme20j  37448  cdleme20l2  37451  cdleme20l  37452  cdleme20m  37453  cdleme22cN  37472  cdleme22d  37473  cdleme22e  37474  cdleme22f  37476  cdleme26fALTN  37492  cdleme26f  37493  cdleme26f2ALTN  37494  cdleme26f2  37495  cdleme27a  37497  cdleme28a  37500  cdlemefs44  37556  cdlemefs45ee  37560  cdleme32b  37572  cdleme32c  37573  cdleme32e  37575  cdleme35sn2aw  37588  cdleme37m  37592  cdleme39n  37596  cdleme40n  37598  cdleme40w  37600  cdleme42k  37614  cdlemeg47rv2  37640  cdlemeg46rjgN  37652  cdlemeg46rgv  37658  cdlemeg46req  37659  cdlemg2fv2  37730  cdlemg17h  37798  cdlemg31b0a  37825  cdlemg27b  37826  cdlemg31d  37830  cdlemg28b  37833  cdlemg28  37834  cdlemg29  37835  cdlemg33a  37836  cdlemg33b  37837  cdlemg33c  37838  cdlemg33d  37839  cdlemg33e  37840  cdlemg44a  37861  cdlemk7u-2N  38018  cdlemk11u-2N  38019  cdlemk12u-2N  38020  cdlemk26-3  38036  cdlemk27-3  38037  cdlemkfid3N  38055  cdlemn2  38325  cdlemn10  38336  cdlemn11c  38339