Theorem breq12d 2627

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 2625	. 2 |- (ph -> (ARC <-> BRC))
3		breq12d.2	. . 3 |- (ph -> C = D)
4	3	breq2d 2626	. 2 |- (ph -> (BRC <-> BRD))
5	2, 4	bitrd 527	1 |- (ph -> (ARC <-> BRD))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 955   class class class wbr 2615

This theorem is referenced by:  3brtr3d 2640  3brtr4d 2641  hbbrd 2655  sbcbrg 2658  pocl 2840  cnvpo 3518  isoeq1 3882  isocnv 3891  caoprord 4051  xpsneng 4425  xpcomeng 4429  xpdom1g 4433  limensuc 4496  pssnn 4522  unfi 4537  infensuc 4621  unidomg 4792  unxpdom 4827  sucxpdom 4829  ltapq 5059  ltmpq 5060  reclem4pr 5142  ltasr 5192  sqgt0sr 5198  pre-axltadd 5272  pre-axmulgt0 5273  ltadd1t 5607  ltadd2t 5608  leadd1t 5609  leadd2t 5610  lesub1t 5643  lesub2t 5644  ltsub1t 5645  ltsub2t 5646  subge0t 5657  lesub0t 5661  ltmul1 5788  ltdiv1 5790  ltmul1t 5796  ltmul2t 5797  lemul2t 5799  lemul1it 5803  lemul1itOLD 5804  ltdiv1t 5815  ltdiv2t 5845  lediv2t 5849  halfpost 5993  uzindOLD 6166  monoord 6244  expwordit 6548  expord2t 6549  expmwordit 6551  sqlecant 6586  bernneq 6597  abstrit 6850  ser1absdiflem 6881  faclbnd 6897  faclbnd3 6899  faclbnd4lem1 6900  faclbnd4lem2 6901  faclbnd4lem3 6902  faclbnd4lem4 6903  faclbnd6 6906  fsumcmp 6993  fsumabs 6996  ser1cmp 7127  ser1cmp2 7130  cvgcmp3cetlem1 7141  cvgcmp3cetlem2 7142  isumcmpi 7167  infcvglem3 7175  geolim 7189  geolim1 7191  cvgratlem1ALT 7199  cvgratlem2ALT 7200  cvgratlem3ALT 7201  cvgratlem1 7202  cvgratlem3 7204  cvgratlem4 7205  efcltlem1 7263  ef1tlub 7341  ef01tlub 7344  absef01tlub 7346  eflegeot 7373  efm1legeot 7375  efcnlem4 7379  ruclem24 7493  ruclem25 7494  ruclem29 7498  infmap2 7541  ismet 7758  ismsg 7760  msflem 7763  mettri2 7773  mettri4 7774  metreslem 7784  bcthlem17 7977  isnvlem 8193  nvi 8197  nvtri 8262  nmlnoubi 8416  nmblolbii 8418  nmblolbi 8419  blocnilem 8423  sii 8473  efifolem5 8676  norm-iit 8960  norm3dift 8972  norm3adift 8975  bcst 9003  occllem2 9129  projlem22 9162  projlem26 9166  pjnormt 9626  pjnelt 9628  nmbdoplb 9905  nmbdoplbt 9906  nmcopexlem3 9909  nmcoplbt 9916  lnopcon 9919  nmbdfnlbt 9935  nmcfnexlem3 9938  nmcfnlbt 9945  lnfncon 9946  pjdifnormt 10051  mdslmd2 10213  cvmdt 10219  cvexcht 10257  cdj1 10316  cdj3lem1 10317  cdj3lem2b 10320  cdj3lem3b 10323  cdj3 10324  lediv2itALT 10327

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-un 2047  df-sn 2409  df-pr 2410  df-op 2413  df-br 2616

Copyright terms: Public domain