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

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

Proof of Theorem simp33l
StepHypRef Expression
1 simp3l 1024 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant3 1019 1  |-  ( ( ta  /\  et  /\  ( ch  /\  th  /\  ( ph  /\  ps )
) )  ->  ph )
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  cdleme19d  35395  cdleme19e  35396  cdleme20h  35405  cdleme20l2  35410  cdleme20m  35412  cdleme21d  35419  cdleme21e  35420  cdleme22e  35433  cdleme22f2  35436  cdleme22g  35437  cdleme26e  35448  cdleme28a  35459  cdleme28b  35460  cdleme37m  35551  cdleme39n  35555  cdlemeg46gfre  35621  cdlemg28a  35782  cdlemg28b  35792  cdlemk3  35922  cdlemk5a  35924  cdlemk6  35926  cdlemkuat  35955  cdlemkid2  36013
  Copyright terms: Public domain W3C validator