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  4665  soisores  5840  omopth2  6598  ramub1lem1  13089  efgsfo  15064  lbspss  15851  llyrest  17227  ptbasin  17288  basqtop  17418  mulcxp  20048  cvmlift2lem10  23858  5segofs  24701  btwnconn1lem13  24794  iccss3  25237  clscnc  26113  jm2.25lem1  27194  2llnjaN  30377  paddasslem12  30642  lhp2lt  30812  lhpexle2lem  30820  lhpmcvr3  30836  lhpat3  30857  trlval3  30998  cdleme17b  31098  cdlemefr27cl  31214  cdlemg11b  31453  tendococl  31583  cdlemj3  31634  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk53b  31767  cdlemk35u  31775  cdlemm10N  31930  dihopelvalcpre  32060  dihord6apre  32068  dihord5b  32071  dihglblem5apreN  32103  dihglblem2N  32106  dihmeetlem6  32121  dihmeetlem18N  32136  dvh3dim2  32260  dvh3dim3N  32261
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