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  24466  cdleme19b  30420  cdleme19e  30423  cdleme20h  30432  cdleme20l2  30437  cdleme20m  30439  cdleme21d  30446  cdleme21e  30447  cdleme22eALTN  30461  cdleme22f2  30463  cdleme22g  30464  cdleme26e  30475  cdleme37m  30578  cdlemeg46gfre  30648  cdlemg28a  30809  cdlemg28b  30819  cdlemk5a  30951  cdlemk6  30953
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