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

Theorem simp13r 1071
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 984 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant1 976 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pceu  12899  axpasch  24569  prdnei  25573  3dimlem4  29653  3atlem4  29675  llncvrlpln2  29746  2lplnja  29808  lhpmcvr5N  30216  4atexlemswapqr  30252  4atexlemnclw  30259  trlval2  30352  cdleme21h  30523  cdleme24  30541  cdleme26ee  30549  cdleme26f  30552  cdleme26f2  30554  cdlemf1  30750  cdlemg16ALTN  30847  cdlemg17iqN  30863  cdlemg27b  30885  trlcone  30917  cdlemg48  30926  tendocan  31013  cdlemk26-3  31095  cdlemk27-3  31096  cdlemk28-3  31097  cdlemk37  31103  cdlemky  31115  cdlemk11ta  31118  cdlemkid3N  31122  cdlemk11t  31135  cdlemk46  31137  cdlemk47  31138  cdlemk51  31142  cdlemk52  31143  cdleml4N  31168  dihmeetlem1N  31480  dihmeetlem20N  31516  mapdpglem32  31895
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator