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

Theorem simpl1r 1010
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 983 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
21adantr 453 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  tfisi  4840  soisores  6049  omopth2  6829  ramub1lem1  13396  efgsfo  15373  lbspss  16156  llyrest  17550  ptbasin  17611  basqtop  17745  ustuqtop1  18273  mulcxp  20578  isarchi2  24257  cvmlift2lem10  25001  5segofs  25942  btwnconn1lem13  26035  jm2.25lem1  27071  2llnjaN  30365  paddasslem12  30630  lhp2lt  30800  lhpexle2lem  30808  lhpmcvr3  30824  lhpat3  30845  trlval3  30986  cdleme17b  31086  cdlemefr27cl  31202  cdlemg11b  31441  tendococl  31571  cdlemj3  31622  cdlemk35s-id  31737  cdlemk39s-id  31739  cdlemk53b  31755  cdlemk35u  31763  cdlemm10N  31918  dihopelvalcpre  32048  dihord6apre  32056  dihord5b  32059  dihglblem5apreN  32091  dihglblem2N  32094  dihmeetlem6  32109  dihmeetlem18N  32124  dvh3dim2  32248  dvh3dim3N  32249
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator