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

Theorem simp13r 1104
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 1017 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant1 1009 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  pceu  13913  axpasch  23187  3dimlem4  33108  3atlem4  33130  llncvrlpln2  33201  2lplnja  33263  lhpmcvr5N  33671  4atexlemswapqr  33707  4atexlemnclw  33714  trlval2  33807  cdleme21h  33978  cdleme24  33996  cdleme26ee  34004  cdleme26f  34007  cdleme26f2  34009  cdlemf1  34205  cdlemg16ALTN  34302  cdlemg17iqN  34318  cdlemg27b  34340  trlcone  34372  cdlemg48  34381  tendocan  34468  cdlemk26-3  34550  cdlemk27-3  34551  cdlemk28-3  34552  cdlemk37  34558  cdlemky  34570  cdlemk11ta  34573  cdlemkid3N  34577  cdlemk11t  34590  cdlemk46  34592  cdlemk47  34593  cdlemk51  34597  cdlemk52  34598  cdleml4N  34623  dihmeetlem1N  34935  dihmeetlem20N  34971  mapdpglem32  35350
  Copyright terms: Public domain W3C validator