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

Theorem simp33r 1085
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 986 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant3 980 1  |-  ( ( ta  /\  et  /\  ( ch  /\  th  /\  ( ph  /\  ps )
) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  totprob  24638  cdleme19b  30786  cdleme19e  30789  cdleme20h  30798  cdleme20l2  30803  cdleme20m  30805  cdleme21d  30812  cdleme21e  30813  cdleme22eALTN  30827  cdleme22f2  30829  cdleme22g  30830  cdleme26e  30841  cdleme37m  30944  cdlemeg46gfre  31014  cdlemg28a  31175  cdlemg28b  31185  cdlemk5a  31317  cdlemk6  31319
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator