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

Theorem breqtrd 3817
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 3805 . 2  |-  ( ph  ->  ( A R B  <-> 
A R C ) )
41, 3mpbid 145 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285   class class class wbr 3793
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-br 3794
This theorem is referenced by:  breqtrrd  3819  syl5breq  3828  tfrexlem  5983  phplem4  6390  phplem4on  6402  fidifsnen  6405  fisbth  6417  fin0  6419  fin0or  6420  ltsonq  6650  addlocprlemeqgt  6784  prmuloclemcalc  6817  mullocprlem  6822  addcanprlemu  6867  ltaprlem  6870  ltaprg  6871  prplnqu  6872  ltmprr  6894  cauappcvgprlemopl  6898  cauappcvgprlemloc  6904  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemloc  6927  caucvgprprlemloccalc  6936  caucvgprprlemopl  6949  recexgt0sr  7012  prsrpos  7023  caucvgsrlemoffgt1  7037  caucvgsr  7040  pitoregt0  7079  add20  7645  mullt0  7651  ltmul1a  7758  ltm1  7991  recgt0  7995  prodgt0gt0  7996  prodgt0  7997  prodge0  7999  lemul1a  8003  recp1lt1  8044  recreclt  8045  ledivp1  8048  mulle0r  8089  ltaddrp2d  8889  fz01en  9148  fzonmapblen  9273  qbtwnrelemcalc  9342  flqaddz  9379  flhalf  9384  flqdiv  9403  modqmuladdim  9449  modqsubdir  9475  addmodlteq  9480  frecfzen2  9509  serile  9571  ltexp2a  9625  leexp2a  9626  exple1  9629  expubnd  9630  bernneq  9690  faclbnd6  9768  cvg1nlemcxze  10006  cvg1nlemres  10009  recvguniqlem  10018  resqrexlemover  10034  resqrexlemdec  10035  resqrexlemcalc2  10039  resqrexlemcalc3  10040  resqrexlemnm  10042  resqrexlemoverl  10045  ltabs  10111  abslt  10112  absle  10113  abstri  10128  maxabslemlub  10231  maxabslemval  10232  dfabsmax  10241  climge0  10301  climaddc2  10306  dvdssub2  10382  dvdsadd2b  10387  dvdsexp  10406  opoe  10439  divalglemeunn  10465  divalglemex  10466  divalglemeuneg  10467  gcdaddm  10519  bezoutlemstep  10530  dvdsgcd  10545  dvdsmulgcd  10558  bezoutr1  10566  nn0seqcvgd  10567  rpmulgcd2  10621  qredeq  10622  rpdvds  10625  prmind2  10646  qdencn  10943
  Copyright terms: Public domain W3C validator