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

Theorem simp33r 1116
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 1017 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant3 1011 1  |-  ( ( ta  /\  et  /\  ( ch  /\  th  /\  ( ph  /\  ps )
) )  ->  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:  totprob  26809  cdleme19b  33946  cdleme19e  33949  cdleme20h  33958  cdleme20l2  33963  cdleme20m  33965  cdleme21d  33972  cdleme21e  33973  cdleme22eALTN  33987  cdleme22f2  33989  cdleme22g  33990  cdleme26e  34001  cdleme37m  34104  cdlemeg46gfre  34174  cdlemg28a  34335  cdlemg28b  34345  cdlemk5a  34477  cdlemk6  34479
  Copyright terms: Public domain W3C validator