MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp33r Structured version   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  24675  cdleme19b  31002  cdleme19e  31005  cdleme20h  31014  cdleme20l2  31019  cdleme20m  31021  cdleme21d  31028  cdleme21e  31029  cdleme22eALTN  31043  cdleme22f2  31045  cdleme22g  31046  cdleme26e  31057  cdleme37m  31160  cdlemeg46gfre  31230  cdlemg28a  31391  cdlemg28b  31401  cdlemk5a  31533  cdlemk6  31535
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