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

Theorem simpl1r 1007
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 980 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
21adantr 451 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  tfisi  4649  soisores  5824  omopth2  6582  ramub1lem1  13073  efgsfo  15048  lbspss  15835  llyrest  17211  ptbasin  17272  basqtop  17402  mulcxp  20032  cvmlift2lem10  23843  5segofs  24629  btwnconn1lem13  24722  iccss3  25134  clscnc  26010  jm2.25lem1  27091  2llnjaN  29755  paddasslem12  30020  lhp2lt  30190  lhpexle2lem  30198  lhpmcvr3  30214  lhpat3  30235  trlval3  30376  cdleme17b  30476  cdlemefr27cl  30592  cdlemg11b  30831  tendococl  30961  cdlemj3  31012  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk53b  31145  cdlemk35u  31153  cdlemm10N  31308  dihopelvalcpre  31438  dihord6apre  31446  dihord5b  31449  dihglblem5apreN  31481  dihglblem2N  31484  dihmeetlem6  31499  dihmeetlem18N  31514  dvh3dim2  31638  dvh3dim3N  31639
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator