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

Theorem simp13r 1115
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 1028 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant1 1020 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 976
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 187  df-an 371  df-3an 978
This theorem is referenced by:  pceu  14581  axpasch  24673  3dimlem4  32494  3atlem4  32516  llncvrlpln2  32587  2lplnja  32649  lhpmcvr5N  33057  4atexlemswapqr  33093  4atexlemnclw  33100  trlval2  33194  cdleme21h  33366  cdleme24  33384  cdleme26ee  33392  cdleme26f  33395  cdleme26f2  33397  cdlemf1  33593  cdlemg16ALTN  33690  cdlemg17iqN  33706  cdlemg27b  33728  trlcone  33760  cdlemg48  33769  tendocan  33856  cdlemk26-3  33938  cdlemk27-3  33939  cdlemk28-3  33940  cdlemk37  33946  cdlemky  33958  cdlemk11ta  33961  cdlemkid3N  33965  cdlemk11t  33978  cdlemk46  33980  cdlemk47  33981  cdlemk51  33985  cdlemk52  33986  cdleml4N  34011  dihmeetlem1N  34323  dihmeetlem20N  34359  mapdpglem32  34738  addlimc  37035
  Copyright terms: Public domain W3C validator