Theorem simp21l 1171

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

Assertion

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

Proof of Theorem simp21l

Step	Hyp	Ref	Expression
1		simp1l 1078	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant2 1076	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  modexp  12861  segconeu  31288  4atlem10  33910  lplncvrlvol2  33919  4atex  34380  4atex2-0cOLDN  34384  cdlemd2  34504  cdlemd3  34505  cdlemd4  34506  cdleme0e  34522  cdleme0moN  34530  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme9  34558  cdleme11c  34566  cdleme11dN  34567  cdleme11e  34568  cdleme11fN  34569  cdleme11h  34571  cdleme11j  34572  cdleme11k  34573  cdleme11  34575  cdleme12  34576  cdleme13  34577  cdleme14  34578  cdleme15a  34579  cdleme15b  34580  cdleme15c  34581  cdleme15d  34582  cdleme15  34583  cdleme16b  34584  cdleme16c  34585  cdleme16d  34586  cdleme16e  34587  cdleme16f  34588  cdleme17d1  34594  cdleme18a  34596  cdleme18b  34597  cdleme18c  34598  cdleme18d  34600  cdleme19b  34610  cdleme19d  34612  cdleme19e  34613  cdleme20c  34617  cdleme20d  34618  cdleme20e  34619  cdleme20f  34620  cdleme20g  34621  cdleme20h  34622  cdleme20j  34624  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme20  34630  cdleme21ct  34635  cdleme21e  34637  cdleme21i  34641  cdleme22aa  34645  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f  34652  cdleme26e  34665  cdleme27a  34673  cdleme32e  34751  cdlemg2fv2  34906  cdlemg4a  34914  cdlemg4d  34919  cdlemg4  34923  cdlemg6c  34926  cdlemg8b  34934  cdlemg8c  34935  cdlemg9a  34938  cdlemg9  34940  cdlemg12a  34949  cdlemg12c  34951  cdlemg17dALTN  34970  cdlemg17h  34974  cdlemg18b  34985  cdlemg18c  34986  cdlemg18d  34987  cdlemg18  34988  cdlemg19a  34989  cdlemg21  34992  cdlemg28a  34999  cdlemg31b0a  35001  cdlemg31d  35006  cdlemg33b0  35007  cdlemg33a  35012  cdlemh  35123  cdlemk5  35142  cdlemk6  35143  cdlemk7  35154  cdlemk11  35155  cdlemk12  35156  cdlemk21N  35179  cdlemk20  35180  cdlemk28-3  35214  cdlemk34  35216  cdlemkfid3N  35231  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk55u1  35271  cdlemn2  35502  cdlemn10  35513  dihjustlem  35523