Theorem breq12d 3351

Description: Equality deduction for a binary relation. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)

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	. 2 |- (ph -> A = B)
2		breq12d.2	. 2 |- (ph -> C = D)
3		breq12 3343	. 2 |- ((A = B /\ C = D) -> (ARC <-> BRD))
4	1, 2, 3	syl11anc 524	1 |- (ph -> (ARC <-> BRD))

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298   class class class wbr 3338

This theorem is referenced by:  breq123d 3353  3brtr3d 3366  3brtr4d 3367  sbcbrgOLD 3391  pocl 3596  vtoclrbr 4033  cnvpo 4427  isoeq1 4863  isocnv 4873  caoprord 4989  xpsneng 5495  xpcomeng 5499  xpdom1g 5503  limensuc 5601  pssnn 5628  unfi 5644  ordiso 5683  infensuc 5745  unidomg 5971  unxpdom 5996  sucxpdom 5998  cdaung 6071  ltapq 6228  ltmpq 6229  reclem4pr 6311  ltasr 6361  sqgt0sr 6367  pre-axltadd 6442  pre-axmulgt0 6443  ltadd1 6806  ltadd2 6807  leadd1 6808  leadd2 6809  lesub1 6849  lesub2 6850  ltsub1 6851  ltsub2 6852  subge0 6863  lesub0 6867  ltmul1i 7000  ltdiv1i 7002  ltmul1 7008  ltmul2 7009  ltmul2OLD 7010  lemul2 7013  lemul2OLD 7014  lemul1a 7019  lemul1aOLD 7020  ltdiv1 7031  ltdiv1OLD 7032  ltdiv2 7070  lediv2 7074  halfpos 7222  uzindOLD 7420  monoord 7523  expwordi 7848  expord2 7849  expmwordi 7851  sqlecan 7887  bernneq 7898  bernneqOLD 7899  abstri 8150  ser1absdiflem 8181  faclbnd 8197  faclbnd3 8199  faclbnd4lem1 8200  faclbnd4lem2 8201  faclbnd4lem3 8202  faclbnd4lem4 8203  faclbnd6 8206  fsumcmp 8300  fsumabs 8303  ser1cmpi 8434  ser1cmp2i 8437  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  isumcmpii 8476  infcvglem3 8484  explecnv 8495  geolim 8499  geolim1 8501  cvgratlem1ALT 8509  cvgratlem2ALT 8510  cvgratlem3ALT 8511  cvgratlem1 8512  cvgratlem3 8514  cvgratlem4 8515  efcltlem1 8566  ef1tlubi 8644  ef01tlubi 8648  absef01tlubi 8650  eflegeo 8681  efm1legeo 8683  efcnlem4 8687  ruclem24 8802  ruclem25 8803  ruclem29 8807  infmap2 8850  ismet 9075  ismsg 9077  msflem 9080  mettri2 9090  mettri4 9091  metreslem 9099  bcthlem17 9293  isnvlem 9561  nvi 9565  nvtri 9630  nmlnoubi 9796  nmblolbii 9799  nmblolbi 9800  blocnilem 9804  sii 9855  efifolem5 10080  dif1en 10172  norm-ii 10638  norm3dif 10650  norm3adifi 10653  bcs 10681  occllem2 10807  projlem22 10840  projlem26 10844  pjnorm 11304  pjnel 11306  nmbdoplbi 11586  nmbdoplb 11587  nmcopexlem3 11590  nmcoplb 11597  lnopconi 11600  nmbdfnlb 11616  nmcfnexlem3 11619  nmcfnlb 11626  lnfnconi 11627  pjdifnormi 11739  mdslmd2i 11902  cvmd 11908  cvexch 11946  cdj1i 12005  cdj3lem1 12006  cdj3lem2b 12009  cdj3lem3b 12012  cdj3i 12013  fndmeng 13598  lediv2aALT 13621  nn0seqcvgd 13659  algcvg 13744  algcvga 13747  eucalglt 13753  eucalgcvga 13754  mulgcdlem5 13760  poseq 13954  sltval2 13997  axdense 14027  axfelem8 14038  axfelem9 14039  axfelem12 14042  domintreflemb 14366  pw2eng 14419  infxpg 14422  preotr2 14576  cntrsetlem 14999  ordisoOLD 15374  ufilen 15579  seqpo 15814  incsequz 15815  fsumlt 15821  fsumltisumi 15823  fsumltisum 15824  fsumleisumi 15826  fsumleisum 15827  trirn 15834  metf1o 15843  mettrifi 15847  geomcau 15849  heiborlem18 15972  heiborlem33 15987  bfplem5 16002  bfplem6 16003  bfplem8 16005  bfplem9 16006  bfplem11 16008  bfp 16009  latjlej2 16867  latmlem2 16877  isopos 16909  oplecon3b 16927  hlatle 17048  pmaple 17241

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-un 2600  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339

Copyright terms: Public domain