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

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

Proof of Theorem eqbrtrd
StepHypRef Expression
1 eqbrtrd.2 . 2  |-  ( ph  ->  B R C )
2 eqbrtrd.1 . . 3  |-  ( ph  ->  A  =  B )
32breq1d 3909 . 2  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
41, 3mpbird 166 1  |-  ( ph  ->  A 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:  eqbrtrrd  3922  dif1en  6741  ccfunen  7047  prarloclemcalc  7278  ltexprlemopu  7379  recexprlemloc  7407  caucvgprprlemloccalc  7460  suplocsrlem  7584  axpre-suploclemres  7677  mulle0r  8666  lbinfle  8672  divge1  9465  xltnegi  9573  xleadd1a  9611  xltadd1  9614  xlt2add  9618  xposdif  9620  xleaddadd  9625  ubmelm1fzo  9958  qbtwnrelemcalc  9988  qbtwnxr  9990  ceiqm1l  10039  ceilqm1lt  10040  ceilqle  10042  modqlt  10061  modqeqmodmin  10122  addmodlteq  10126  exp3vallem  10249  bernneq  10367  faclbnd2  10443  resqrexlemdec  10738  resqrexlemcalc2  10742  resqrexlemglsq  10749  resqrexlemga  10750  abslt  10815  amgm2  10845  icodiamlt  10907  maxabsle  10931  maxltsup  10945  minmax  10956  min1inf  10958  min2inf  10959  bdtrilem  10965  xrmaxltsup  10982  xrmaxaddlem  10984  xrmaxadd  10985  xrminmax  10989  xrmin1inf  10991  xrmin2inf  10992  climconst  11014  serclim0  11029  mulcn2  11036  reccn2ap  11037  iserex  11063  climlec2  11065  iserge0  11067  climcau  11071  climcvg1nlem  11073  fsumabs  11189  iserabs  11199  isumlessdc  11220  divcnv  11221  expcnvre  11227  absgtap  11234  georeclim  11237  cvgratnnlembern  11247  cvgratnnlemsumlt  11252  cvgratnnlemfm  11253  cvgratnnlemrate  11254  mertenslemub  11258  mertenslemi1  11259  efcvgfsum  11287  eftlub  11310  eflegeo  11322  tanval3ap  11335  tannegap  11349  ef01bndlem  11377  sin01bnd  11378  cos01bnd  11379  cos01gt0  11383  mulgcd  11616  eucalglt  11650  lcmledvds  11663  mulgcddvds  11687  prmind2  11713  pw2dvdslemn  11754  pw2dvdseulemle  11756  oddpwdclemdvds  11759  sqrt2irrap  11769  divdenle  11786  nonsq  11796  ennnfonelemkh  11836  bl2in  12483  xblcntrps  12493  xblcntr  12494  ssblps  12505  ssbl  12506  blssps  12507  blss  12508  xmetxp  12587  mulc1cncf  12656  cncfmptc  12662  mulcncflem  12670  ivthinclemlopn  12694  ivthinclemuopn  12696  ivthdec  12702  limcimolemlt  12713  cnplimclemle  12717  cnplimclemr  12718  limccnp2lem  12725  dveflem  12766  qdencn  13118  cvgcmp2nlemabs  13123  trilpolemclim  13125  trilpolemisumle  13127  trilpolemeq1  13129
  Copyright terms: Public domain W3C validator