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  35414  lplncvrlvol2  35423  4atex  35884  4atex2-0cOLDN  35888  cdlemd2  36008  cdlemd3  36009  cdlemd4  36010  cdleme0e  36026  cdleme0moN  36034  cdleme3g  36043  cdleme3h  36044  cdleme3  36046  cdleme9  36062  cdleme11c  36070  cdleme11dN  36071  cdleme11e  36072  cdleme11fN  36073  cdleme11h  36075  cdleme11j  36076  cdleme11k  36077  cdleme11  36079  cdleme12  36080  cdleme13  36081  cdleme14  36082  cdleme15a  36083  cdleme15b  36084  cdleme15c  36085  cdleme15d  36086  cdleme15  36087  cdleme16b  36088  cdleme16c  36089  cdleme16d  36090  cdleme16e  36091  cdleme16f  36092  cdleme17d1  36098  cdleme18a  36100  cdleme18b  36101  cdleme18c  36102  cdleme18d  36104  cdleme19b  36113  cdleme19d  36115  cdleme19e  36116  cdleme20c  36120  cdleme20d  36121  cdleme20e  36122  cdleme20f  36123  cdleme20g  36124  cdleme20h  36125  cdleme20j  36127  cdleme20l2  36130  cdleme20l  36131  cdleme20m  36132  cdleme20  36133  cdleme21ct  36138  cdleme21e  36140  cdleme21i  36144  cdleme22aa  36148  cdleme22cN  36151  cdleme22d  36152  cdleme22e  36153  cdleme22eALTN  36154  cdleme22f  36155  cdleme26e  36168  cdleme27a  36176  cdleme32e  36254  cdlemg2fv2  36409  cdlemg4a  36417  cdlemg4d  36422  cdlemg4  36426  cdlemg6c  36429  cdlemg8b  36437  cdlemg8c  36438  cdlemg9a  36441  cdlemg9  36443  cdlemg12a  36452  cdlemg12c  36454  cdlemg17dALTN  36473  cdlemg17h  36477  cdlemg18b  36488  cdlemg18c  36489  cdlemg18d  36490  cdlemg18  36491  cdlemg19a  36492  cdlemg21  36495  cdlemg28a  36502  cdlemg31b0a  36504  cdlemg31d  36509  cdlemg33b0  36510  cdlemg33a  36515  cdlemh  36626  cdlemk5  36645  cdlemk6  36646  cdlemk7  36657  cdlemk11  36658  cdlemk12  36659  cdlemk21N  36682  cdlemk20  36683  cdlemk28-3  36717  cdlemk34  36719  cdlemkfid3N  36734  cdlemk35s-id  36747  cdlemk39s-id  36749  cdlemk55u1  36774  cdlemn2  37005  cdlemn10  37016  dihjustlem  37026
  Copyright terms: Public domain W3C validator