Theorem breq12d 3888

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof 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 -> ( A R C <-> B R D ) )

Proof of Theorem breq12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 |- ( ph -> A = B )
2		breq12d.2	. 2 |- ( ph -> C = D )
3		breq12 3880	. 2 |- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
4	1, 2, 3	syl2anc 406	1 |- ( ph -> ( A R C <-> B R D ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1299   class class class wbr 3875

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483  df-br 3876

This theorem is referenced by:  breq123d  3889  3brtr3d  3904  3brtr4d  3905  pocl  4163  csbcnvg  4661  cnvpom  5017  sbcfung  5083  isoeq1  5634  isocnv  5644  isotr  5649  caovordig  5868  caovordg  5870  caovord2d  5872  caovord  5874  ofrfval  5922  ofrval  5924  ofrfval2  5929  caofref  5934  fundmeng  6631  xpsneng  6645  xpcomeng  6651  xpdom2g  6655  phplem3g  6679  php5  6681  php5dom  6686  nqtri3or  7105  ltsonq  7107  ltanqg  7109  ltmnqg  7110  lt2addnq  7113  lt2mulnq  7114  prarloclemarch  7127  ltrnqg  7129  ltnnnq  7132  prarloclemlt  7202  addlocprlemgt  7243  mullocprlem  7279  addextpr  7330  recexprlemss1l  7344  recexprlemss1u  7345  recexpr  7347  caucvgprlemcanl  7353  cauappcvgprlemm  7354  cauappcvgprlemdisj  7360  cauappcvgprlemloc  7361  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  cauappcvgprlem1  7368  cauappcvgprlemlim  7370  cauappcvgpr  7371  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemdisj  7383  caucvgprlemloc  7384  caucvgprlemcl  7385  caucvgprlemladdrl  7387  caucvgprlem1  7388  caucvgpr  7391  caucvgprprlemell  7394  caucvgprprlemcbv  7396  caucvgprprlemval  7397  caucvgprprlemnkeqj  7399  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemloc  7412  caucvgprprlemclphr  7414  caucvgprprlemexb  7416  caucvgprprlem1  7418  lttrsr  7458  ltposr  7459  ltsosr  7460  ltasrg  7466  aptisr  7474  mulextsr1lem  7475  mulextsr1  7476  caucvgsrlemcau  7488  caucvgsrlemgt1  7490  caucvgsrlemoffcau  7493  caucvgsrlemoffres  7495  caucvgsr  7497  axpre-ltirr  7567  axpre-ltadd  7571  axpre-mulgt0  7572  axpre-mulext  7573  axcaucvglemcau  7583  axcaucvglemres  7584  ltadd2  8048  ltadd1  8058  leadd2  8060  reapval  8204  reapmul1  8223  remulext2  8228  apreim  8231  apirr  8233  apsym  8234  apcotr  8235  apadd1  8236  apadd2  8237  apneg  8239  mulext1  8240  mulext2  8241  apti  8250  apsub1  8269  subap0  8270  apmul1  8409  apmul2  8410  apdivmuld  8434  ltmul2  8472  lemul2  8473  ltdiv1  8484  ltdiv2  8503  ledivdiv  8506  lediv2  8507  negiso  8571  div4p1lem1div2  8825  qapne  9281  nn0ledivnn  9395  xleadd1  9499  xltadd1  9500  xltadd2  9501  xsubge0  9505  xleaddadd  9511  qtri3or  9861  frecfzennn  10040  monoord  10090  monoord2  10091  leexp1a  10189  bernneq  10253  nn0le2msqd  10306  faclbnd  10328  faclbnd3  10330  faclbnd6  10331  facubnd  10332  fihashdom  10390  zfz1isolemiso  10423  cjap  10519  cvg1nlemcau  10596  cvg1nlemres  10597  resqrexlemlo  10625  resqrexlemcalc3  10628  absext  10675  xrnegiso  10870  xrminltinf  10880  fsumabs  11073  cvgratnnlemnexp  11132  cvgratnnlemmn  11133  addmodlteqALT  11352  nn0seqcvgd  11515  algcvg  11522  algcvga  11525  eucalgcvga  11532  qnumgt0  11668  ctinfomlemom  11732  ispsmet  12251  psmettri2  12256  ismet  12272  isxmet  12273  xmettri2  12289  blvalps  12316  blval  12317  comet  12427  bdxmet  12429