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

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

Proof of Theorem simp13r
StepHypRef Expression
1 simp3r 1025 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant1 1017 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ps )
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:  pceu  14225  axpasch  23920  addlimc  31190  3dimlem4  34260  3atlem4  34282  llncvrlpln2  34353  2lplnja  34415  lhpmcvr5N  34823  4atexlemswapqr  34859  4atexlemnclw  34866  trlval2  34959  cdleme21h  35130  cdleme24  35148  cdleme26ee  35156  cdleme26f  35159  cdleme26f2  35161  cdlemf1  35357  cdlemg16ALTN  35454  cdlemg17iqN  35470  cdlemg27b  35492  trlcone  35524  cdlemg48  35533  tendocan  35620  cdlemk26-3  35702  cdlemk27-3  35703  cdlemk28-3  35704  cdlemk37  35710  cdlemky  35722  cdlemk11ta  35725  cdlemkid3N  35729  cdlemk11t  35742  cdlemk46  35744  cdlemk47  35745  cdlemk51  35749  cdlemk52  35750  cdleml4N  35775  dihmeetlem1N  36087  dihmeetlem20N  36123  mapdpglem32  36502
  Copyright terms: Public domain W3C validator