Theorem breq12d 4057

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 4049	. 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 4044

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4045

This theorem is referenced by:  breq123d  4058  3brtr3d  4075  3brtr4d  4076  pocl  4350  csbcnvg  4862  cnvpom  5225  sbcfung  5295  isoeq1  5870  isocnv  5880  isotr  5885  caovordig  6112  caovordg  6114  caovord2d  6116  caovord  6118  ofrfval  6167  ofrval  6169  ofrfval2  6175  caofref  6183  fundmeng  6899  xpsneng  6917  xpcomeng  6923  xpdom2g  6927  phplem3g  6953  php5  6955  php5dom  6960  exmidpw2en  7009  exmidapne  7372  nqtri3or  7509  ltsonq  7511  ltanqg  7513  ltmnqg  7514  lt2addnq  7517  lt2mulnq  7518  prarloclemarch  7531  ltrnqg  7533  ltnnnq  7536  prarloclemlt  7606  addlocprlemgt  7647  mullocprlem  7683  addextpr  7734  recexprlemss1l  7748  recexprlemss1u  7749  recexpr  7751  caucvgprlemcanl  7757  cauappcvgprlemm  7758  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  cauappcvgprlemlim  7774  cauappcvgpr  7775  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemcl  7789  caucvgprlemladdrl  7791  caucvgprlem1  7792  caucvgpr  7795  caucvgprprlemell  7798  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemnkeqj  7803  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemloc  7816  caucvgprprlemclphr  7818  caucvgprprlemexb  7820  caucvgprprlem1  7822  lttrsr  7875  ltposr  7876  ltsosr  7877  ltasrg  7883  aptisr  7892  mulextsr1lem  7893  mulextsr1  7894  caucvgsrlemcau  7906  caucvgsrlemgt1  7908  caucvgsrlemoffcau  7911  caucvgsrlemoffres  7913  caucvgsr  7915  axpre-ltirr  7995  axpre-ltadd  7999  axpre-mulgt0  8000  axpre-mulext  8001  axcaucvglemcau  8011  axcaucvglemres  8012  ltadd2  8492  ltadd1  8502  leadd2  8504  reapval  8649  reapmul1  8668  remulext2  8673  apreim  8676  apirr  8678  apsym  8679  apcotr  8680  apadd1  8681  apadd2  8682  apneg  8684  mulext1  8685  mulext2  8686  apti  8695  apsub1  8715  subap0  8716  apmul1  8861  apmul2  8862  apdivmuld  8886  ltmul2  8929  lemul2  8930  ltdiv1  8941  ltdiv2  8960  ledivdiv  8963  lediv2  8964  negiso  9028  div4p1lem1div2  9291  qapne  9760  nn0ledivnn  9889  xleadd1  9997  xltadd1  9998  xltadd2  9999  xsubge0  10003  xleaddadd  10009  qtri3or  10383  frecfzennn  10571  monoord  10630  monoord2  10631  leexp1a  10739  bernneq  10805  apexp1  10863  nn0le2msqd  10864  faclbnd  10886  faclbnd3  10888  faclbnd6  10889  facubnd  10890  fihashdom  10948  zfz1isolemiso  10984  cjap  11217  cvg1nlemcau  11295  cvg1nlemres  11296  resqrexlemlo  11324  resqrexlemcalc3  11327  absext  11374  xrnegiso  11573  xrminltinf  11583  fsumabs  11776  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  fprodle  11951  addmodlteqALT  12170  nn0seqcvgd  12363  algcvg  12370  algcvga  12373  eucalgcvga  12380  qnumgt0  12520  pcprendvds2  12614  pcpremul  12616  pcadd2  12664  2expltfac  12762  ctinfomlemom  12798  gsumfzval  13223  mplsubgfilemcl  14461  ispsmet  14795  psmettri2  14800  ismet  14816  isxmet  14817  xmettri2  14833  blvalps  14860  blval  14861  comet  14971  bdxmet  14973  dvef  15199  cxplt  15388  rpcxple2  15390  rpcxplt2  15391  cxplt3  15392  apcxp2  15411  ltexp2  15413  logbleb  15433  logblt  15434  lgsdilem  15504  2lgslem1a2  15564  apdifflemr  15990  apdiff  15991