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

Theorem simp21l 1075
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp21l  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ph )

Proof of Theorem simp21l
StepHypRef Expression
1 simp1l 982 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant2 980 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  modexp  11552  segconeu  25980  4atlem10  30577  lplncvrlvol2  30586  4atex  31047  4atex2-0cOLDN  31051  cdlemd2  31170  cdlemd3  31171  cdlemd4  31172  cdleme0e  31188  cdleme0moN  31196  cdleme3g  31205  cdleme3h  31206  cdleme3  31208  cdleme9  31224  cdleme11c  31232  cdleme11dN  31233  cdleme11e  31234  cdleme11fN  31235  cdleme11h  31237  cdleme11j  31238  cdleme11k  31239  cdleme11  31241  cdleme12  31242  cdleme13  31243  cdleme14  31244  cdleme15a  31245  cdleme15b  31246  cdleme15c  31247  cdleme15d  31248  cdleme15  31249  cdleme16b  31250  cdleme16c  31251  cdleme16d  31252  cdleme16e  31253  cdleme16f  31254  cdleme17d1  31260  cdleme18a  31262  cdleme18b  31263  cdleme18c  31264  cdleme18d  31266  cdleme19b  31275  cdleme19d  31277  cdleme19e  31278  cdleme20c  31282  cdleme20d  31283  cdleme20e  31284  cdleme20f  31285  cdleme20g  31286  cdleme20h  31287  cdleme20j  31289  cdleme20l2  31292  cdleme20l  31293  cdleme20m  31294  cdleme20  31295  cdleme21ct  31300  cdleme21e  31302  cdleme21i  31306  cdleme22aa  31310  cdleme22cN  31313  cdleme22d  31314  cdleme22e  31315  cdleme22eALTN  31316  cdleme22f  31317  cdleme26e  31330  cdleme27a  31338  cdleme32e  31416  cdlemg2fv2  31571  cdlemg4a  31579  cdlemg4d  31584  cdlemg4  31588  cdlemg6c  31591  cdlemg8b  31599  cdlemg8c  31600  cdlemg9a  31603  cdlemg9  31605  cdlemg12a  31614  cdlemg12c  31616  cdlemg17dALTN  31635  cdlemg17h  31639  cdlemg18b  31650  cdlemg18c  31651  cdlemg18d  31652  cdlemg18  31653  cdlemg19a  31654  cdlemg21  31657  cdlemg28a  31664  cdlemg31b0a  31666  cdlemg31d  31671  cdlemg33b0  31672  cdlemg33a  31677  cdlemh  31788  cdlemk5  31807  cdlemk6  31808  cdlemk7  31819  cdlemk11  31820  cdlemk12  31821  cdlemk21N  31844  cdlemk20  31845  cdlemk28-3  31879  cdlemk34  31881  cdlemkfid3N  31896  cdlemk35s-id  31909  cdlemk39s-id  31911  cdlemk55u1  31936  cdlemn2  32167  cdlemn10  32178  dihjustlem  32188
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator