ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  breqtrd Unicode version

Theorem breqtrd 3954
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
Hypotheses
Ref Expression
breqtrd.1  |-  ( ph  ->  A R B )
breqtrd.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
breqtrd  |-  ( ph  ->  A R C )

Proof of Theorem breqtrd
StepHypRef Expression
1 breqtrd.1 . 2  |-  ( ph  ->  A R B )
2 breqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32breq2d 3941 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 146 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331   class class class wbr 3929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930
This theorem is referenced by:  breqtrrd  3956  breqtrid  3965  tfrexlem  6231  phplem4  6749  phplem4on  6761  fidifsnen  6764  fisbth  6777  fin0  6779  fin0or  6780  ltsonq  7218  addlocprlemeqgt  7352  prmuloclemcalc  7385  mullocprlem  7390  addcanprlemu  7435  ltaprlem  7438  ltaprg  7439  prplnqu  7440  ltmprr  7462  cauappcvgprlemopl  7466  cauappcvgprlemloc  7472  cauappcvgprlemladdru  7476  cauappcvgprlemladdrl  7477  cauappcvgprlem1  7479  caucvgprlemm  7488  caucvgprlemopl  7489  caucvgprlemloc  7495  caucvgprprlemloccalc  7504  caucvgprprlemopl  7517  recexgt0sr  7593  ltm1sr  7597  prsrpos  7605  caucvgsrlemoffgt1  7619  caucvgsr  7622  suplocsrlempr  7627  pitoregt0  7669  axpre-suploclemres  7721  add20  8248  mullt0  8254  ltmul1a  8365  ltm1  8616  recgt0  8620  prodgt0gt0  8621  prodgt0  8622  prodge0  8624  lemul1a  8628  recp1lt1  8669  recreclt  8670  ledivp1  8673  mulle0r  8714  ltaddrp2d  9530  mul2lt0np  9562  xleadd1a  9668  xleaddadd  9682  fz01en  9845  fzonmapblen  9976  qbtwnrelemcalc  10045  flqaddz  10082  flhalf  10087  flqdiv  10106  modqmuladdim  10152  modqsubdir  10178  addmodlteq  10183  frecfzen2  10212  iseqf1olemab  10274  ser3le  10303  ltexp2a  10357  leexp2a  10358  exple1  10361  expubnd  10362  bernneq  10424  faclbnd6  10502  hashfz  10579  zfz1isolemiso  10594  zfz1iso  10596  seq3coll  10597  cvg1nlemcxze  10766  cvg1nlemres  10769  recvguniqlem  10778  resqrexlemover  10794  resqrexlemdec  10795  resqrexlemcalc2  10799  resqrexlemcalc3  10800  resqrexlemnm  10802  resqrexlemoverl  10805  ltabs  10871  abslt  10872  absle  10873  abstri  10888  maxabslemlub  10991  maxabslemval  10992  dfabsmax  11001  bdtrilem  11022  xrmaxiflemab  11028  xrmaxiflemlub  11029  xrmaxaddlem  11041  reccn2ap  11094  climge0  11106  climaddc2  11111  summodclem2a  11162  zsumdc  11165  isumge0  11211  fsumle  11244  fsumlt  11245  isumshft  11271  expcnvap0  11283  geolim  11292  geolim2  11293  georeclim  11294  geo2lim  11297  cvgratnnlembern  11304  cvgratnnlemfm  11310  mertenslemi1  11316  mertensabs  11318  prodmodclem3  11356  prodmodclem2a  11357  efcllemp  11376  ef0lem  11378  efgt0  11402  eftlub  11408  efltim  11416  sinbnd  11470  cosbnd  11471  ef01bndlem  11474  sin01gt0  11479  cos01gt0  11480  sin02gt0  11481  eirraplem  11494  dvdssub2  11546  dvdsadd2b  11551  dvdsexp  11570  opoe  11603  divalglemeunn  11629  divalglemex  11630  divalglemeuneg  11631  gcdaddm  11683  bezoutlemstep  11696  dvdsgcd  11711  dvdsmulgcd  11724  bezoutr1  11732  nn0seqcvgd  11733  rpmulgcd2  11787  qredeq  11788  rpdvds  11791  prmind2  11812  divdenle  11886  phicl2  11901  hashdvds  11908  phimullem  11912  ennnfonelemkh  11936  ennnfonelemnn0  11946  psmetsym  12512  psmettri  12513  mettri2  12545  xmetsym  12551  xmettri  12555  metrtri  12560  xblss2ps  12587  xblss2  12588  blhalf  12591  xmsge0  12650  cnmet  12713  ivthinclemlopn  12797  dveflem  12870  dvef  12871  sin0pilem1  12884  sinq12gt0  12933  sinq34lt0t  12934  cosq14gt0  12935  coseq0q4123  12937  pwf1oexmid  13253  qdencn  13283  cvgcmp2nlemabs  13288  apdifflemf  13300  apdifflemr  13301
  Copyright terms: Public domain W3C validator