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

Theorem simp13r 1074
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 987 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant1 979 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  pceu  13221  axpasch  25881  3dimlem4  30262  3atlem4  30284  llncvrlpln2  30355  2lplnja  30417  lhpmcvr5N  30825  4atexlemswapqr  30861  4atexlemnclw  30868  trlval2  30961  cdleme21h  31132  cdleme24  31150  cdleme26ee  31158  cdleme26f  31161  cdleme26f2  31163  cdlemf1  31359  cdlemg16ALTN  31456  cdlemg17iqN  31472  cdlemg27b  31494  trlcone  31526  cdlemg48  31535  tendocan  31622  cdlemk26-3  31704  cdlemk27-3  31705  cdlemk28-3  31706  cdlemk37  31712  cdlemky  31724  cdlemk11ta  31727  cdlemkid3N  31731  cdlemk11t  31744  cdlemk46  31746  cdlemk47  31747  cdlemk51  31751  cdlemk52  31752  cdleml4N  31777  dihmeetlem1N  32089  dihmeetlem20N  32125  mapdpglem32  32504
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator