Theorem breq12d 4000

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 3992	. 2 |- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
4	1, 2, 3	syl2anc 409	1 |- ( ph -> ( A R C <-> B R D ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   class class class wbr 3987

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-br 3988

This theorem is referenced by:  breq123d  4001  3brtr3d  4018  3brtr4d  4019  pocl  4286  csbcnvg  4793  cnvpom  5151  sbcfung  5220  isoeq1  5777  isocnv  5787  isotr  5792  caovordig  6015  caovordg  6017  caovord2d  6019  caovord  6021  ofrfval  6066  ofrval  6068  ofrfval2  6074  caofref  6079  fundmeng  6781  xpsneng  6796  xpcomeng  6802  xpdom2g  6806  phplem3g  6830  php5  6832  php5dom  6837  nqtri3or  7345  ltsonq  7347  ltanqg  7349  ltmnqg  7350  lt2addnq  7353  lt2mulnq  7354  prarloclemarch  7367  ltrnqg  7369  ltnnnq  7372  prarloclemlt  7442  addlocprlemgt  7483  mullocprlem  7519  addextpr  7570  recexprlemss1l  7584  recexprlemss1u  7585  recexpr  7587  caucvgprlemcanl  7593  cauappcvgprlemm  7594  cauappcvgprlemdisj  7600  cauappcvgprlemloc  7601  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  cauappcvgprlem1  7608  cauappcvgprlemlim  7610  cauappcvgpr  7611  caucvgprlemnkj  7615  caucvgprlemnbj  7616  caucvgprlemdisj  7623  caucvgprlemloc  7624  caucvgprlemcl  7625  caucvgprlemladdrl  7627  caucvgprlem1  7628  caucvgpr  7631  caucvgprprlemell  7634  caucvgprprlemcbv  7636  caucvgprprlemval  7637  caucvgprprlemnkeqj  7639  caucvgprprlemopl  7646  caucvgprprlemlol  7647  caucvgprprlemloc  7652  caucvgprprlemclphr  7654  caucvgprprlemexb  7656  caucvgprprlem1  7658  lttrsr  7711  ltposr  7712  ltsosr  7713  ltasrg  7719  aptisr  7728  mulextsr1lem  7729  mulextsr1  7730  caucvgsrlemcau  7742  caucvgsrlemgt1  7744  caucvgsrlemoffcau  7747  caucvgsrlemoffres  7749  caucvgsr  7751  axpre-ltirr  7831  axpre-ltadd  7835  axpre-mulgt0  7836  axpre-mulext  7837  axcaucvglemcau  7847  axcaucvglemres  7848  ltadd2  8325  ltadd1  8335  leadd2  8337  reapval  8482  reapmul1  8501  remulext2  8506  apreim  8509  apirr  8511  apsym  8512  apcotr  8513  apadd1  8514  apadd2  8515  apneg  8517  mulext1  8518  mulext2  8519  apti  8528  apsub1  8548  subap0  8549  apmul1  8692  apmul2  8693  apdivmuld  8717  ltmul2  8759  lemul2  8760  ltdiv1  8771  ltdiv2  8790  ledivdiv  8793  lediv2  8794  negiso  8858  div4p1lem1div2  9118  qapne  9585  nn0ledivnn  9711  xleadd1  9819  xltadd1  9820  xltadd2  9821  xsubge0  9825  xleaddadd  9831  qtri3or  10186  frecfzennn  10369  monoord  10419  monoord2  10420  leexp1a  10518  bernneq  10583  apexp1  10639  nn0le2msqd  10640  faclbnd  10662  faclbnd3  10664  faclbnd6  10665  facubnd  10666  fihashdom  10725  zfz1isolemiso  10761  cjap  10857  cvg1nlemcau  10935  cvg1nlemres  10936  resqrexlemlo  10964  resqrexlemcalc3  10967  absext  11014  xrnegiso  11212  xrminltinf  11222  fsumabs  11415  cvgratnnlemnexp  11474  cvgratnnlemmn  11475  fprodle  11590  addmodlteqALT  11806  nn0seqcvgd  11982  algcvg  11989  algcvga  11992  eucalgcvga  11999  qnumgt0  12139  pcprendvds2  12232  pcpremul  12234  ctinfomlemom  12369  ispsmet  13038  psmettri2  13043  ismet  13059  isxmet  13060  xmettri2  13076  blvalps  13103  blval  13104  comet  13214  bdxmet  13216  dvef  13403  cxplt  13551  rpcxple2  13553  rpcxplt2  13554  cxplt3  13555  apcxp2  13573  ltexp2  13575  logbleb  13594  logblt  13595  lgsdilem  13643  apdifflemr  14001  apdiff  14002