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

Theorem simp13r 1122
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 1035 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant1 1027 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  pceu  14789  axpasch  24963  3dimlem4  32954  3atlem4  32976  llncvrlpln2  33047  2lplnja  33109  lhpmcvr5N  33517  4atexlemswapqr  33553  4atexlemnclw  33560  trlval2  33654  cdleme21h  33826  cdleme24  33844  cdleme26ee  33852  cdleme26f  33855  cdleme26f2  33857  cdlemf1  34053  cdlemg16ALTN  34150  cdlemg17iqN  34166  cdlemg27b  34188  trlcone  34220  cdlemg48  34229  tendocan  34316  cdlemk26-3  34398  cdlemk27-3  34399  cdlemk28-3  34400  cdlemk37  34406  cdlemky  34418  cdlemk11ta  34421  cdlemkid3N  34425  cdlemk11t  34438  cdlemk46  34440  cdlemk47  34441  cdlemk51  34445  cdlemk52  34446  cdleml4N  34471  dihmeetlem1N  34783  dihmeetlem20N  34819  mapdpglem32  35198  addlimc  37555
  Copyright terms: Public domain W3C validator