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

Theorem simpl1r 1040
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 1013 . 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 965
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 967
This theorem is referenced by:  soisores  6016  tfisi  6467  omopth2  7021  repswswrd  12420  ramub1lem1  14085  efgsfo  16234  lbspss  17161  maducoeval2  18444  madurid  18448  llyrest  19087  ptbasin  19148  basqtop  19282  ustuqtop1  19814  mulcxp  22128  br8d  25940  isarchi2  26200  archiabllem2c  26210  cvmlift2lem10  27199  5segofs  28035  btwnconn1lem13  28128  jm2.25lem1  29344  pmatcollpw1dstlem1  30897  mp2pm2mplem4  30916  2llnjaN  33207  paddasslem12  33472  lhp2lt  33642  lhpexle2lem  33650  lhpmcvr3  33666  lhpat3  33687  trlval3  33828  cdleme17b  33928  cdlemefr27cl  34044  cdlemg11b  34283  tendococl  34413  cdlemj3  34464  cdlemk35s-id  34579  cdlemk39s-id  34581  cdlemk53b  34597  cdlemk35u  34605  cdlemm10N  34760  dihopelvalcpre  34890  dihord6apre  34898  dihord5b  34901  dihglblem5apreN  34933  dihglblem2N  34936  dihmeetlem6  34951  dihmeetlem18N  34966  dvh3dim2  35090  dvh3dim3N  35091
  Copyright terms: Public domain W3C validator