Theorem simp23l 1182

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

Assertion

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

Proof of Theorem simp23l

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  ax5seglem6  25814  lshpkrlem5  34401  lplnexllnN  34850  4atexlemt  35339  4atex2  35363  4atex3  35367  trlval4  35475  cdlemc5  35482  cdlemc6  35483  cdlemd2  35486  cdleme0e  35504  cdleme0moN  35512  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme4  35525  cdleme5  35527  cdleme9  35540  cdleme11fN  35551  cdleme11j  35554  cdleme11k  35555  cdleme11l  35556  cdleme11  35557  cdleme14  35560  cdleme15a  35561  cdleme15b  35562  cdleme15c  35563  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme17d1  35576  cdleme18c  35580  cdlemednpq  35586  cdleme19c  35593  cdleme20bN  35598  cdleme20d  35600  cdleme20f  35602  cdleme20g  35603  cdleme20h  35604  cdleme20j  35606  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22f  35634  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme27a  35655  cdleme28a  35658  cdlemefs44  35714  cdlemefs45ee  35718  cdleme32b  35730  cdleme32c  35731  cdleme32e  35733  cdleme35sn2aw  35746  cdleme37m  35750  cdleme39n  35754  cdleme40n  35756  cdleme40w  35758  cdleme42k  35772  cdlemeg47rv2  35798  cdlemeg46rjgN  35810  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemg2fv2  35888  cdlemg17h  35956  cdlemg31b0a  35983  cdlemg27b  35984  cdlemg31d  35988  cdlemg28b  35991  cdlemg28  35992  cdlemg29  35993  cdlemg33a  35994  cdlemg33b  35995  cdlemg33c  35996  cdlemg33d  35997  cdlemg33e  35998  cdlemg44a  36019  cdlemk7u-2N  36176  cdlemk11u-2N  36177  cdlemk12u-2N  36178  cdlemk26-3  36194  cdlemk27-3  36195  cdlemkfid3N  36213  cdlemn2  36484  cdlemn10  36495  cdlemn11c  36498