MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl1r Structured version   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  4830  soisores  6039  omopth2  6819  ramub1lem1  13386  efgsfo  15363  lbspss  16146  llyrest  17540  ptbasin  17601  basqtop  17735  ustuqtop1  18263  mulcxp  20568  isarchi2  24247  cvmlift2lem10  24991  5segofs  25932  btwnconn1lem13  26025  jm2.25lem1  27060  2llnjaN  30300  paddasslem12  30565  lhp2lt  30735  lhpexle2lem  30743  lhpmcvr3  30759  lhpat3  30780  trlval3  30921  cdleme17b  31021  cdlemefr27cl  31137  cdlemg11b  31376  tendococl  31506  cdlemj3  31557  cdlemk35s-id  31672  cdlemk39s-id  31674  cdlemk53b  31690  cdlemk35u  31698  cdlemm10N  31853  dihopelvalcpre  31983  dihord6apre  31991  dihord5b  31994  dihglblem5apreN  32026  dihglblem2N  32029  dihmeetlem6  32044  dihmeetlem18N  32059  dvh3dim2  32183  dvh3dim3N  32184
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