Theorem breq12d 4067

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1373   class class class wbr 4054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-br 4055

This theorem is referenced by:  breq123d  4068  3brtr3d  4085  3brtr4d  4086  pocl  4363  csbcnvg  4875  cnvpom  5239  sbcfung  5309  isoeq1  5888  isocnv  5898  isotr  5903  caovordig  6130  caovordg  6132  caovord2d  6134  caovord  6136  ofrfval  6185  ofrval  6187  ofrfval2  6193  caofref  6201  fundmeng  6918  xpsneng  6937  xpcomeng  6943  xpdom2g  6947  phplem3g  6973  php5  6975  php5dom  6980  exmidpw2en  7030  exmidapne  7402  nqtri3or  7539  ltsonq  7541  ltanqg  7543  ltmnqg  7544  lt2addnq  7547  lt2mulnq  7548  prarloclemarch  7561  ltrnqg  7563  ltnnnq  7566  prarloclemlt  7636  addlocprlemgt  7677  mullocprlem  7713  addextpr  7764  recexprlemss1l  7778  recexprlemss1u  7779  recexpr  7781  caucvgprlemcanl  7787  cauappcvgprlemm  7788  cauappcvgprlemdisj  7794  cauappcvgprlemloc  7795  cauappcvgprlemladdru  7799  cauappcvgprlemladdrl  7800  cauappcvgprlem1  7802  cauappcvgprlemlim  7804  cauappcvgpr  7805  caucvgprlemnkj  7809  caucvgprlemnbj  7810  caucvgprlemdisj  7817  caucvgprlemloc  7818  caucvgprlemcl  7819  caucvgprlemladdrl  7821  caucvgprlem1  7822  caucvgpr  7825  caucvgprprlemell  7828  caucvgprprlemcbv  7830  caucvgprprlemval  7831  caucvgprprlemnkeqj  7833  caucvgprprlemopl  7840  caucvgprprlemlol  7841  caucvgprprlemloc  7846  caucvgprprlemclphr  7848  caucvgprprlemexb  7850  caucvgprprlem1  7852  lttrsr  7905  ltposr  7906  ltsosr  7907  ltasrg  7913  aptisr  7922  mulextsr1lem  7923  mulextsr1  7924  caucvgsrlemcau  7936  caucvgsrlemgt1  7938  caucvgsrlemoffcau  7941  caucvgsrlemoffres  7943  caucvgsr  7945  axpre-ltirr  8025  axpre-ltadd  8029  axpre-mulgt0  8030  axpre-mulext  8031  axcaucvglemcau  8041  axcaucvglemres  8042  ltadd2  8522  ltadd1  8532  leadd2  8534  reapval  8679  reapmul1  8698  remulext2  8703  apreim  8706  apirr  8708  apsym  8709  apcotr  8710  apadd1  8711  apadd2  8712  apneg  8714  mulext1  8715  mulext2  8716  apti  8725  apsub1  8745  subap0  8746  apmul1  8891  apmul2  8892  apdivmuld  8916  ltmul2  8959  lemul2  8960  ltdiv1  8971  ltdiv2  8990  ledivdiv  8993  lediv2  8994  negiso  9058  div4p1lem1div2  9321  qapne  9790  nn0ledivnn  9919  xleadd1  10027  xltadd1  10028  xltadd2  10029  xsubge0  10033  xleaddadd  10039  qtri3or  10415  frecfzennn  10603  monoord  10662  monoord2  10663  leexp1a  10771  bernneq  10837  apexp1  10895  nn0le2msqd  10896  faclbnd  10918  faclbnd3  10920  faclbnd6  10921  facubnd  10922  fihashdom  10980  zfz1isolemiso  11016  cjap  11302  cvg1nlemcau  11380  cvg1nlemres  11381  resqrexlemlo  11409  resqrexlemcalc3  11412  absext  11459  xrnegiso  11658  xrminltinf  11668  fsumabs  11861  cvgratnnlemnexp  11920  cvgratnnlemmn  11921  fprodle  12036  addmodlteqALT  12255  nn0seqcvgd  12448  algcvg  12455  algcvga  12458  eucalgcvga  12465  qnumgt0  12605  pcprendvds2  12699  pcpremul  12701  pcadd2  12749  2expltfac  12847  ctinfomlemom  12883  gsumfzval  13308  mplsubgfilemcl  14546  ispsmet  14880  psmettri2  14885  ismet  14901  isxmet  14902  xmettri2  14918  blvalps  14945  blval  14946  comet  15056  bdxmet  15058  dvef  15284  cxplt  15473  rpcxple2  15475  rpcxplt2  15476  cxplt3  15477  apcxp2  15496  ltexp2  15498  logbleb  15518  logblt  15519  lgsdilem  15589  2lgslem1a2  15649  apdifflemr  16158  apdiff  16159