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

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

Proof of Theorem simp23r
StepHypRef Expression
1 simp3r 984 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant2 977 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ax5seglem6  24562  lshpkrlem5  29304  lplnexllnN  29753  4atexlemutvt  30243  cdlemc5  30384  cdlemd2  30388  cdleme0moN  30414  cdleme3h  30424  cdleme5  30429  cdleme9  30442  cdleme11l  30458  cdleme14  30462  cdleme15c  30465  cdleme16b  30468  cdleme16d  30470  cdleme16e  30471  cdlemednpq  30488  cdleme20bN  30499  cdleme20j  30507  cdleme20l2  30510  cdleme20l  30511  cdleme22cN  30531  cdleme22d  30532  cdleme22e  30533  cdleme22f  30535  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme27a  30556  cdleme32b  30631  cdleme32d  30633  cdleme32f  30635  cdleme39n  30655  cdleme40n  30657  cdlemg2fv2  30789  cdlemg17h  30857  cdlemg27b  30885  cdlemg28b  30892  cdlemg28  30893  cdlemg29  30894  cdlemg33a  30895  cdlemg33d  30898  cdlemk7u-2N  31077  cdlemk11u-2N  31078  cdlemk12u-2N  31079  cdlemk26-3  31095  cdlemk27-3  31096  cdlemkfid3N  31114  cdlemn11c  31399
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