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

Theorem simp23r 1110
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 1017 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant2 1010 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  ax5seglem6  23331  lshpkrlem5  33082  lplnexllnN  33531  4atexlemutvt  34021  cdlemc5  34162  cdlemd2  34166  cdleme0moN  34192  cdleme3h  34202  cdleme5  34207  cdleme9  34220  cdleme11l  34236  cdleme14  34240  cdleme15c  34243  cdleme16b  34246  cdleme16d  34248  cdleme16e  34249  cdlemednpq  34266  cdleme20bN  34277  cdleme20j  34285  cdleme20l2  34288  cdleme20l  34289  cdleme22cN  34309  cdleme22d  34310  cdleme22e  34311  cdleme22f  34313  cdleme26fALTN  34329  cdleme26f  34330  cdleme26f2ALTN  34331  cdleme26f2  34332  cdleme27a  34334  cdleme32b  34409  cdleme32d  34411  cdleme32f  34413  cdleme39n  34433  cdleme40n  34435  cdlemg2fv2  34567  cdlemg17h  34635  cdlemg27b  34663  cdlemg28b  34670  cdlemg28  34671  cdlemg29  34672  cdlemg33a  34673  cdlemg33d  34676  cdlemk7u-2N  34855  cdlemk11u-2N  34856  cdlemk12u-2N  34857  cdlemk26-3  34873  cdlemk27-3  34874  cdlemkfid3N  34892  cdlemn11c  35177
  Copyright terms: Public domain W3C validator