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

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

Proof of Theorem simp21l
StepHypRef Expression
1 simp1l 1247 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
213ad2ant2 1157 1 ((𝜏 ∧ ((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  modexp  13218  segconeu  32437  4atlem10  35384  lplncvrlvol2  35393  4atex  35854  4atex2-0cOLDN  35858  cdlemd2  35977  cdlemd3  35978  cdlemd4  35979  cdleme0e  35995  cdleme0moN  36003  cdleme3g  36012  cdleme3h  36013  cdleme3  36015  cdleme9  36031  cdleme11c  36039  cdleme11dN  36040  cdleme11e  36041  cdleme11fN  36042  cdleme11h  36044  cdleme11j  36045  cdleme11k  36046  cdleme11  36048  cdleme12  36049  cdleme13  36050  cdleme14  36051  cdleme15a  36052  cdleme15b  36053  cdleme15c  36054  cdleme15d  36055  cdleme15  36056  cdleme16b  36057  cdleme16c  36058  cdleme16d  36059  cdleme16e  36060  cdleme16f  36061  cdleme17d1  36067  cdleme18a  36069  cdleme18b  36070  cdleme18c  36071  cdleme18d  36073  cdleme19b  36082  cdleme19d  36084  cdleme19e  36085  cdleme20c  36089  cdleme20d  36090  cdleme20e  36091  cdleme20f  36092  cdleme20g  36093  cdleme20h  36094  cdleme20j  36096  cdleme20l2  36099  cdleme20l  36100  cdleme20m  36101  cdleme20  36102  cdleme21ct  36107  cdleme21e  36109  cdleme21i  36113  cdleme22aa  36117  cdleme22cN  36120  cdleme22d  36121  cdleme22e  36122  cdleme22eALTN  36123  cdleme22f  36124  cdleme26e  36137  cdleme27a  36145  cdleme32e  36223  cdlemg2fv2  36378  cdlemg4a  36386  cdlemg4d  36391  cdlemg4  36395  cdlemg6c  36398  cdlemg8b  36406  cdlemg8c  36407  cdlemg9a  36410  cdlemg9  36412  cdlemg12a  36421  cdlemg12c  36423  cdlemg17dALTN  36442  cdlemg17h  36446  cdlemg18b  36457  cdlemg18c  36458  cdlemg18d  36459  cdlemg18  36460  cdlemg19a  36461  cdlemg21  36464  cdlemg28a  36471  cdlemg31b0a  36473  cdlemg31d  36478  cdlemg33b0  36479  cdlemg33a  36484  cdlemh  36595  cdlemk5  36614  cdlemk6  36615  cdlemk7  36626  cdlemk11  36627  cdlemk12  36628  cdlemk21N  36651  cdlemk20  36652  cdlemk28-3  36686  cdlemk34  36688  cdlemkfid3N  36703  cdlemk35s-id  36716  cdlemk39s-id  36718  cdlemk55u1  36743  cdlemn2  36973  cdlemn10  36984  dihjustlem  36994
  Copyright terms: Public domain W3C validator