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

Theorem simpl1r 1048
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl1r  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta )  ->  ps )

Proof of Theorem simpl1r
StepHypRef Expression
1 simp1r 1021 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
21adantr 465 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  soisores  6209  tfisi  6671  omopth2  7230  repswswrd  12713  ramub1lem1  14396  efgsfo  16550  lbspss  17508  maducoeval2  18906  madurid  18910  decpmatmullem  19036  mp2pm2mplem4  19074  llyrest  19749  ptbasin  19810  basqtop  19944  ustuqtop1  20476  mulcxp  22791  br8d  27133  isarchi2  27388  archiabllem2c  27398  cvmlift2lem10  28394  5segofs  29230  btwnconn1lem13  29323  jm2.25lem1  30544  limcleqr  31186  icccncfext  31226  fourierdlem87  31494  2llnjaN  34362  paddasslem12  34627  lhp2lt  34797  lhpexle2lem  34805  lhpmcvr3  34821  lhpat3  34842  trlval3  34983  cdleme17b  35083  cdlemefr27cl  35199  cdlemg11b  35438  tendococl  35568  cdlemj3  35619  cdlemk35s-id  35734  cdlemk39s-id  35736  cdlemk53b  35752  cdlemk35u  35760  cdlemm10N  35915  dihopelvalcpre  36045  dihord6apre  36053  dihord5b  36056  dihglblem5apreN  36088  dihglblem2N  36091  dihmeetlem6  36106  dihmeetlem18N  36121  dvh3dim2  36245  dvh3dim3N  36246
  Copyright terms: Public domain W3C validator