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  4651  soisores  5826  omopth2  6584  ramub1lem1  13075  efgsfo  15050  lbspss  15837  llyrest  17213  ptbasin  17274  basqtop  17404  mulcxp  20034  cvmlift2lem10  23845  5segofs  24631  btwnconn1lem13  24724  iccss3  25145  clscnc  26021  jm2.25lem1  27102  2llnjaN  29828  paddasslem12  30093  lhp2lt  30263  lhpexle2lem  30271  lhpmcvr3  30287  lhpat3  30308  trlval3  30449  cdleme17b  30549  cdlemefr27cl  30665  cdlemg11b  30904  tendococl  31034  cdlemj3  31085  cdlemk35s-id  31200  cdlemk39s-id  31202  cdlemk53b  31218  cdlemk35u  31226  cdlemm10N  31381  dihopelvalcpre  31511  dihord6apre  31519  dihord5b  31522  dihglblem5apreN  31554  dihglblem2N  31557  dihmeetlem6  31572  dihmeetlem18N  31587  dvh3dim2  31711  dvh3dim3N  31712
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