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

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

Proof of Theorem eqbrtrrd
StepHypRef Expression
1 eqbrtrrd.1 . . 3  |-  ( ph  ->  A  =  B )
21eqcomd 2123 . 2  |-  ( ph  ->  B  =  A )
3 eqbrtrrd.2 . 2  |-  ( ph  ->  A R C )
42, 3eqbrtrd 3920 1  |-  ( ph  ->  B R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316   class class class wbr 3899
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900
This theorem is referenced by:  dftpos4  6128  phpm  6727  unsnfidcex  6776  fisseneq  6788  f1finf1o  6803  prmuloclemcalc  7341  mullocprlem  7346  cauappcvgprlemladdfl  7431  caucvgprlemopl  7445  caucvgprprlemloccalc  7460  caucvgprprlemopl  7473  ltadd1sr  7552  suplocsrlem  7584  axarch  7667  axpre-suploclemres  7677  lemulge11  8592  mul2lt0llt0  9516  mul2lt0lgt0  9517  mul2lt0pn  9519  xaddge0  9629  modqmuladdim  10108  ltexp2a  10313  leexp2a  10314  nnlesq  10364  faclbnd6  10458  facavg  10460  fiprsshashgt1  10531  cvg1nlemcxze  10722  resqrexlemover  10750  resqrexlemlo  10753  resqrexlemnmsq  10757  resqrexlemnm  10758  leabs  10814  abs3dif  10845  abs2dif  10846  maxabslemlub  10947  maxltsup  10958  bdtri  10979  xrmaxiflemab  10984  xrbdtri  11013  recn2  11054  imcn2  11055  iserex  11076  summodclem2a  11118  fsumge1  11198  isumrpcl  11231  cvgratnnlemseq  11263  cvgratnnlemsumlt  11265  mertenslemi1  11272  ege2le3  11304  efgt1p2  11328  efgt1p  11329  tanval2ap  11347  tanval3ap  11348  cos12dec  11401  eirraplem  11410  divalglemnqt  11544  mulgcd  11631  dvdssqlem  11645  nn0seqcvgd  11649  mulgcddvds  11702  rpdvds  11707  pw2dvdseulemle  11772  sqrt2irraplemnn  11784  qden1elz  11810  phimullem  11828  hashgcdlem  11830  hashgcdeq  11831  ennnfonelemex  11854  lmcn2  12376  psmetge0  12427  xmetge0  12461  cnopnap  12690  suplociccex  12699  ivthinclemlopn  12710  ivthinclemuopn  12712  cnplimclemr  12734  limccnp2lem  12741  dveflem  12782  cosq23lt0  12841  coseq0q4123  12842  cosq34lt1  12858  taupi  13166
  Copyright terms: Public domain W3C validator