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

Theorem breqtrrd 3956
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 2145 . 2  |-  ( ph  ->  B  =  C )
41, 3breqtrd 3954 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:  frirrg  4272  unsnfidcex  6808  unsnfidcel  6809  addlocprlemeq  7348  ltexprlemopl  7416  recexprlemloc  7446  cauappcvgprlemopl  7461  cauappcvgprlemladdfu  7469  cauappcvgprlem1  7474  caucvgprlemopl  7484  caucvgprlemladdfu  7492  caucvgprprlemopl  7512  caucvgprprlemexbt  7521  mulgt0sr  7593  archsr  7597  caucvgsrlemoffgt1  7614  suplocsrlemb  7621  suplocsrlem  7623  mulap0r  8384  prodgt0  8617  div4p1lem1div2  8980  mul2lt0rgt0  9554  xleadd1a  9663  xltadd1  9666  xlt2add  9670  xposdif  9672  xlesubadd  9673  xleaddadd  9677  uzsubsubfz  9834  fzctr  9917  subfzo0  10026  exbtwnzlemstep  10032  exbtwnzlemex  10034  rebtwn2zlemstep  10037  rebtwn2z  10039  qbtwnxr  10042  ceilqge  10090  modqge0  10112  modqlt  10113  modqid  10129  m1modge3gt1  10151  modaddmodup  10167  addmodlteq  10178  ser3mono  10258  ser3ge0  10297  ser3le  10298  leexp1a  10355  sqgt0ap  10368  sqge0  10376  nnlesq  10403  expnbnd  10422  nn0opthlem2d  10474  facwordi  10493  filtinf  10545  hashunlem  10557  zfz1isolemiso  10589  cjmulge0  10668  resqrexlemover  10789  resqrexlemdec  10790  resqrexlemlo  10792  resqrexlemcalc3  10795  resqrexlemcvg  10798  resqrexlemoverl  10800  resqrexlemglsq  10801  resqrexlemga  10802  absge0  10839  amgm2  10897  maxle1  10990  bdtrilem  11017  xrmaxifle  11022  xrmaxiflemlub  11024  xrmaxiflemval  11026  xrmax1sup  11029  xrmaxltsup  11034  xrmaxadd  11037  xrbdtri  11052  reccn2ap  11089  climle  11110  climserle  11121  isumclim2  11198  isumclim3  11199  isumge0  11206  fsumlessfi  11236  expcnvap0  11278  expcnvre  11279  explecnv  11281  absltap  11285  cvgratnnlembern  11299  cvgratnnlemnexp  11300  cvgratnnlemmn  11301  cvgratnnlemabsle  11303  cvgratnnlemfm  11305  cvgratnnlemrate  11306  mertenslemi1  11311  mertenslem2  11312  clim2divap  11316  prodmodclem3  11351  efcvg  11379  ege2le3  11384  efaddlem  11387  eftlub  11403  effsumlt  11405  ef01bndlem  11470  sin02gt0  11477  eirrap  11491  iddvdsexp  11524  dvdsadd  11543  dvdsfac  11565  dvdsmod  11567  omoe  11600  divalglemnn  11622  divalglemnqt  11624  flodddiv4t2lthalf  11641  dvdslegcd  11660  dfgcd3  11705  dvdssqim  11719  dvdsmulgcd  11720  nn0seqcvgd  11729  dvdslcm  11757  lcmgcdlem  11765  mulgcddvds  11782  qredeq  11784  cncongr2  11792  sqnprm  11823  isprm6  11832  sqpweven  11860  znege1  11863  sqrt2irrap  11865  nonsq  11892  hashdvds  11904  ennnfonelemkh  11932  psmetxrge0  12511  isxmet2d  12527  mettri  12552  xmettri3  12553  mettri3  12554  xblss2ps  12583  blss2ps  12585  blss2  12586  blssps  12606  blss  12607  xmetxp  12686  ivthdec  12801  sin0pilem1  12875  sinq12gt0  12924  tangtx  12932  cosordlem  12943  cosq34lt1  12944  cvgcmp2nlemabs  13257  trilpolemclim  13259  trilpolemeq1  13263  apdifflemf  13267  apdifflemr  13268
  Copyright terms: Public domain W3C validator