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

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

Proof of Theorem simp23l
StepHypRef Expression
1 simp3l 983 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant2 977 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ax5seglem6  25121  lshpkrlem5  29373  lplnexllnN  29822  4atexlemt  30311  4atex2  30335  4atex3  30339  trlval4  30446  cdlemc5  30453  cdlemc6  30454  cdlemd2  30457  cdleme0e  30475  cdleme0moN  30483  cdleme3g  30492  cdleme3h  30493  cdleme3  30495  cdleme4  30496  cdleme5  30498  cdleme9  30511  cdleme11fN  30522  cdleme11j  30525  cdleme11k  30526  cdleme11l  30527  cdleme11  30528  cdleme14  30531  cdleme15a  30532  cdleme15b  30533  cdleme15c  30534  cdleme16b  30537  cdleme16c  30538  cdleme16d  30539  cdleme16e  30540  cdleme16f  30541  cdleme17d1  30547  cdleme18c  30551  cdlemednpq  30557  cdleme19c  30563  cdleme20bN  30568  cdleme20d  30570  cdleme20f  30572  cdleme20g  30573  cdleme20h  30574  cdleme20j  30576  cdleme20l2  30579  cdleme20l  30580  cdleme20m  30581  cdleme22cN  30600  cdleme22d  30601  cdleme22e  30602  cdleme22f  30604  cdleme26fALTN  30620  cdleme26f  30621  cdleme26f2ALTN  30622  cdleme26f2  30623  cdleme27a  30625  cdleme28a  30628  cdlemefs44  30684  cdlemefs45ee  30688  cdleme32b  30700  cdleme32c  30701  cdleme32e  30703  cdleme35sn2aw  30716  cdleme37m  30720  cdleme39n  30724  cdleme40n  30726  cdleme40w  30728  cdleme42k  30742  cdlemeg47rv2  30768  cdlemeg46rjgN  30780  cdlemeg46rgv  30786  cdlemeg46req  30787  cdlemg2fv2  30858  cdlemg17h  30926  cdlemg31b0a  30953  cdlemg27b  30954  cdlemg31d  30958  cdlemg28b  30961  cdlemg28  30962  cdlemg29  30963  cdlemg33a  30964  cdlemg33b  30965  cdlemg33c  30966  cdlemg33d  30967  cdlemg33e  30968  cdlemg44a  30989  cdlemk7u-2N  31146  cdlemk11u-2N  31147  cdlemk12u-2N  31148  cdlemk26-3  31164  cdlemk27-3  31165  cdlemkfid3N  31183  cdlemn2  31454  cdlemn10  31465  cdlemn11c  31468
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator