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

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

Proof of Theorem simp33r
StepHypRef Expression
1 simp3r 1025 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant3 1019 1  |-  ( ( ta  /\  et  /\  ( ch  /\  th  /\  ( ph  /\  ps )
) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  totprob  28159  cdleme19b  35393  cdleme19e  35396  cdleme20h  35405  cdleme20l2  35410  cdleme20m  35412  cdleme21d  35419  cdleme21e  35420  cdleme22eALTN  35434  cdleme22f2  35436  cdleme22g  35437  cdleme26e  35448  cdleme37m  35551  cdlemeg46gfre  35621  cdlemg28a  35782  cdlemg28b  35792  cdlemk5a  35924  cdlemk6  35926
  Copyright terms: Public domain W3C validator