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

Theorem simpl1r 1048
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl1r

Proof of Theorem simpl1r
StepHypRef Expression
1 simp1r 1021 . 2
21adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  soisores  6223  tfisi  6693  omopth2  7252  repswswrd  12756  ramub1lem1  14544  efgsfo  16757  lbspss  17728  maducoeval2  19142  madurid  19146  decpmatmullem  19272  mp2pm2mplem4  19310  llyrest  19986  ptbasin  20078  basqtop  20212  ustuqtop1  20744  mulcxp  23066  br8d  27463  isarchi2  27729  archiabllem2c  27739  cvmlift2lem10  28757  5segofs  29656  btwnconn1lem13  29749  jm2.25lem1  30940  limcleqr  31650  icccncfext  31690  fourierdlem87  31976  2llnjaN  35290  paddasslem12  35555  lhp2lt  35725  lhpexle2lem  35733  lhpmcvr3  35749  lhpat3  35770  trlval3  35912  cdleme17b  36012  cdlemefr27cl  36129  cdlemg11b  36368  tendococl  36498  cdlemj3  36549  cdlemk35s-id  36664  cdlemk39s-id  36666  cdlemk53b  36682  cdlemk35u  36690  cdlemm10N  36845  dihopelvalcpre  36975  dihord6apre  36983  dihord5b  36986  dihglblem5apreN  37018  dihglblem2N  37021  dihmeetlem6  37036  dihmeetlem18N  37051  dvh3dim2  37175  dvh3dim3N  37176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator