Theorem breq12d 2621

Description: Equality deduction for a binary relation.

Hypotheses

Ref	Expression
breq1d.1	|- (ph -> A = B)
breq12d.2	|- (ph -> C = D)

Assertion

Ref	Expression
breq12d	|- (ph -> (ARC <-> BRD))

Proof of Theorem breq12d

Step	Hyp	Ref	Expression
1		breq1d.1	. . 3 |- (ph -> A = B)
2	1	breq1d 2619	. 2 |- (ph -> (ARC <-> BRC))
3		breq12d.2	. . 3 |- (ph -> C = D)
4	3	breq2d 2620	. 2 |- (ph -> (BRC <-> BRD))
5	2, 4	bitrd 526	1 |- (ph -> (ARC <-> BRD))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953   class class class wbr 2609

This theorem is referenced by:  3brtr3d 2634  3brtr4d 2635  hbbrd 2649  sbcbrg 2652  pocl 2835  cnvpo 3508  isoeq1 3872  isocnv 3881  caoprord 4042  xpsneng 4416  xpcomeng 4420  xpdom1g 4424  limensuc 4487  pssnn 4513  unfi 4528  infensuc 4610  unidomg 4781  unxpdom 4816  sucxpdom 4818  ltapq 5048  ltmpq 5049  reclem4pr 5131  ltasr 5181  sqgt0sr 5187  pre-axltadd 5261  pre-axmulgt0 5262  ltadd1t 5597  ltadd2t 5598  leadd1t 5599  leadd2t 5600  lesub1t 5633  lesub2t 5634  ltsub1t 5635  ltsub2t 5636  subge0t 5647  lesub0t 5651  ltmul1 5778  ltdiv1 5780  ltmul1t 5786  ltmul2t 5787  lemul2t 5789  lemul1it 5793  lemul1itOLD 5794  ltdiv1t 5805  ltdiv2t 5835  lediv2t 5839  halfpost 5983  uzindOLD 6156  monoord 6231  expwordit 6534  expord2t 6535  expmwordit 6537  sqlecant 6572  bernneq 6583  abstrit 6835  ser1absdiflem 6866  faclbnd 6882  faclbnd3 6884  faclbnd4lem1 6885  faclbnd4lem2 6886  faclbnd4lem3 6887  faclbnd4lem4 6888  faclbnd6 6891  fsumcmp 6978  fsumabs 6981  ser1cmp 7110  ser1cmp2 7113  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  isumcmpi 7150  infcvglem3 7158  geolim 7172  geolim1 7174  cvgratlem1ALT 7182  cvgratlem2ALT 7183  cvgratlem3ALT 7184  cvgratlem1 7185  cvgratlem3 7187  cvgratlem4 7188  efcltlem1 7246  ef1tlub 7324  ef01tlub 7327  absef01tlub 7329  eflegeot 7356  efm1legeot 7358  efcnlem4 7362  ruclem24 7476  ruclem25 7477  ruclem29 7481  infmap2 7523  ismet 7737  ismsg 7739  msflem 7742  mettri2 7752  mettri4 7753  metreslem 7762  bcthlem17 7949  isnvlem 8167  isnvgOLD 8168  nvi 8173  nvtri 8237  nmlnoubi 8388  nmblolbii 8390  nmblolbi 8391  blocnilem 8395  sii 8445  efifolem5 8641  norm-iit 8926  norm3dift 8938  norm3adift 8941  bcst 8969  occllem2 9090  projlem22 9123  projlem26 9127  pjnormt 9586  pjnelt 9588  nmbdoplb 9864  nmbdoplbt 9865  nmcopexlem3 9868  nmcoplbt 9875  lnopcon 9878  nmbdfnlbt 9894  nmcfnexlem3 9897  nmcfnlbt 9904  lnfncon 9905  pjdifnormt 10006  mdslmd2 10165  cvmdt 10171  cvexcht 10209  cdj1 10265  cdj3lem1 10266  cdj3lem2b 10269  cdj3lem3b 10272  cdj3 10273  lediv2itALT 10276

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610

Copyright terms: Public domain