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

Theorem simpl1r 1009
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 982 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
21adantr 452 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  tfisi  4778  soisores  5986  omopth2  6763  ramub1lem1  13321  efgsfo  15298  lbspss  16081  llyrest  17469  ptbasin  17530  basqtop  17664  ustuqtop1  18192  mulcxp  20443  cvmlift2lem10  24778  5segofs  25654  btwnconn1lem13  25747  jm2.25lem1  26760  2llnjaN  29680  paddasslem12  29945  lhp2lt  30115  lhpexle2lem  30123  lhpmcvr3  30139  lhpat3  30160  trlval3  30301  cdleme17b  30401  cdlemefr27cl  30517  cdlemg11b  30756  tendococl  30886  cdlemj3  30937  cdlemk35s-id  31052  cdlemk39s-id  31054  cdlemk53b  31070  cdlemk35u  31078  cdlemm10N  31233  dihopelvalcpre  31363  dihord6apre  31371  dihord5b  31374  dihglblem5apreN  31406  dihglblem2N  31409  dihmeetlem6  31424  dihmeetlem18N  31439  dvh3dim2  31563  dvh3dim3N  31564
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator