MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp21l Structured version   Visualization version   GIF version

Theorem simp21l 1374
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp21l ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜂) → 𝜑)

Proof of Theorem simp21l
StepHypRef Expression
1 simp1l 1239 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
213ad2ant2 1128 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  modexp  13206  segconeu  32455  4atlem10  35415  lplncvrlvol2  35424  4atex  35885  4atex2-0cOLDN  35889  cdlemd2  36009  cdlemd3  36010  cdlemd4  36011  cdleme0e  36027  cdleme0moN  36035  cdleme3g  36044  cdleme3h  36045  cdleme3  36047  cdleme9  36063  cdleme11c  36071  cdleme11dN  36072  cdleme11e  36073  cdleme11fN  36074  cdleme11h  36076  cdleme11j  36077  cdleme11k  36078  cdleme11  36080  cdleme12  36081  cdleme13  36082  cdleme14  36083  cdleme15a  36084  cdleme15b  36085  cdleme15c  36086  cdleme15d  36087  cdleme15  36088  cdleme16b  36089  cdleme16c  36090  cdleme16d  36091  cdleme16e  36092  cdleme16f  36093  cdleme17d1  36099  cdleme18a  36101  cdleme18b  36102  cdleme18c  36103  cdleme18d  36105  cdleme19b  36114  cdleme19d  36116  cdleme19e  36117  cdleme20c  36121  cdleme20d  36122  cdleme20e  36123  cdleme20f  36124  cdleme20g  36125  cdleme20h  36126  cdleme20j  36128  cdleme20l2  36131  cdleme20l  36132  cdleme20m  36133  cdleme20  36134  cdleme21ct  36139  cdleme21e  36141  cdleme21i  36145  cdleme22aa  36149  cdleme22cN  36152  cdleme22d  36153  cdleme22e  36154  cdleme22eALTN  36155  cdleme22f  36156  cdleme26e  36169  cdleme27a  36177  cdleme32e  36255  cdlemg2fv2  36410  cdlemg4a  36418  cdlemg4d  36423  cdlemg4  36427  cdlemg6c  36430  cdlemg8b  36438  cdlemg8c  36439  cdlemg9a  36442  cdlemg9  36444  cdlemg12a  36453  cdlemg12c  36455  cdlemg17dALTN  36474  cdlemg17h  36478  cdlemg18b  36489  cdlemg18c  36490  cdlemg18d  36491  cdlemg18  36492  cdlemg19a  36493  cdlemg21  36496  cdlemg28a  36503  cdlemg31b0a  36505  cdlemg31d  36510  cdlemg33b0  36511  cdlemg33a  36516  cdlemh  36627  cdlemk5  36646  cdlemk6  36647  cdlemk7  36658  cdlemk11  36659  cdlemk12  36660  cdlemk21N  36683  cdlemk20  36684  cdlemk28-3  36718  cdlemk34  36720  cdlemkfid3N  36735  cdlemk35s-id  36748  cdlemk39s-id  36750  cdlemk55u1  36775  cdlemn2  37005  cdlemn10  37016  dihjustlem  37026
  Copyright terms: Public domain W3C validator