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

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

Proof of Theorem breqtrrd
StepHypRef Expression
1 breqtrrd.1 . 2  |-  ( ph  ->  A R B )
2 breqtrrd.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2087 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 3817 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:  frirrg  4113  unsnfidcex  6440  unsnfidcel  6441  addlocprlemeq  6785  ltexprlemopl  6853  recexprlemloc  6883  cauappcvgprlemopl  6898  cauappcvgprlemladdfu  6906  cauappcvgprlem1  6911  caucvgprlemopl  6921  caucvgprlemladdfu  6929  caucvgprprlemopl  6949  caucvgprprlemexbt  6958  mulgt0sr  7016  archsr  7020  caucvgsrlemoffgt1  7037  mulap0r  7782  prodgt0  7997  div4p1lem1div2  8351  uzsubsubfz  9142  fzctr  9221  subfzo0  9328  exbtwnzlemstep  9334  exbtwnzlemex  9336  rebtwn2zlemstep  9339  rebtwn2z  9341  qbtwnxr  9344  ceilqge  9392  modqge0  9414  modqlt  9415  modqid  9431  m1modge3gt1  9453  modaddmodup  9469  addmodlteq  9480  isermono  9553  serile  9571  leexp1a  9628  sqgt0ap  9641  sqge0  9649  nnlesq  9675  expnbnd  9693  nn0opthlem2d  9745  facwordi  9764  filtinf  9816  sizeunlem  9828  cjmulge0  9914  resqrexlemover  10034  resqrexlemdec  10035  resqrexlemlo  10037  resqrexlemcalc3  10040  resqrexlemcvg  10043  resqrexlemoverl  10045  resqrexlemglsq  10046  resqrexlemga  10047  absge0  10084  amgm2  10142  maxle1  10235  climle  10310  climserile  10321  iddvdsexp  10364  dvdsadd  10383  dvdsfac  10405  dvdsmod  10407  omoe  10440  divalglemnn  10462  divalglemnqt  10464  flodddiv4t2lthalf  10481  dvdslegcd  10500  dfgcd3  10543  dvdssqim  10557  dvdsmulgcd  10558  nn0seqcvgd  10567  dvdslcm  10595  lcmgcdlem  10603  mulgcddvds  10620  qredeq  10622  cncongr2  10630  sqnprm  10661  isprm6  10670  sqpweven  10697  znege1  10700  sqrt2irrap  10702
  Copyright terms: Public domain W3C validator