Theorem breq12d 4138

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1402   class class class wbr 4125

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-br 4126

This theorem is referenced by:  breq123d  4139  3brtr3d  4156  3brtr4d  4157  pocl  4443  csbcnvg  4959  cnvpom  5325  sbcfung  5396  isoeq1  5997  isocnv  6007  isotr  6012  caovordig  6245  caovordg  6247  caovord2d  6249  caovord  6251  ofrfval  6301  ofrval  6303  ofrfval2  6309  caofref  6317  fundmeng  7085  xpsneng  7110  xpcomeng  7116  xpdom2g  7120  phplem3g  7147  php5  7149  php5dom  7154  exmidpw2en  7209  papirr  7601  exmidapne  7616  nqtri3or  7753  ltsonq  7755  ltanqg  7757  ltmnqg  7758  lt2addnq  7761  lt2mulnq  7762  prarloclemarch  7775  ltrnqg  7777  ltnnnq  7780  prarloclemlt  7850  addlocprlemgt  7891  mullocprlem  7927  addextpr  7978  recexprlemss1l  7992  recexprlemss1u  7993  recexpr  7995  caucvgprlemcanl  8001  cauappcvgprlemm  8002  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  cauappcvgprlemlim  8018  cauappcvgpr  8019  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemcl  8033  caucvgprlemladdrl  8035  caucvgprlem1  8036  caucvgpr  8039  caucvgprprlemell  8042  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemnkeqj  8047  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemloc  8060  caucvgprprlemclphr  8062  caucvgprprlemexb  8064  caucvgprprlem1  8066  lttrsr  8119  ltposr  8120  ltsosr  8121  ltasrg  8127  aptisr  8136  mulextsr1lem  8137  mulextsr1  8138  caucvgsrlemcau  8150  caucvgsrlemgt1  8152  caucvgsrlemoffcau  8155  caucvgsrlemoffres  8157  caucvgsr  8159  axpre-ltirr  8239  axpre-ltadd  8243  axpre-mulgt0  8244  axpre-mulext  8245  axcaucvglemcau  8255  axcaucvglemres  8256  ltadd2  8737  ltadd1  8747  leadd2  8749  reapval  8894  reapmul1  8913  remulext2  8918  apreim  8921  apirr  8923  apsym  8924  apcotr  8925  apadd1  8926  apadd2  8927  apneg  8929  mulext1  8930  mulext2  8931  apti  8940  apsub1  8960  subap0  8961  apmul1  9108  apmul2  9109  apdivmuld  9133  ltmul2  9176  lemul2  9177  ltdiv1  9188  ltdiv2  9207  ledivdiv  9210  lediv2  9211  negiso  9275  div4p1lem1div2  9538  qapne  10018  nn0ledivnn  10147  xleadd1  10256  xltadd1  10257  xltadd2  10258  xsubge0  10262  xleaddadd  10268  qtri3or  10653  frecfzennn  10841  monoord  10900  monoord2  10901  leexp1a  11009  bernneq  11076  apexp1  11134  nn0le2msqd  11135  faclbnd  11157  faclbnd3  11159  faclbnd6  11160  facubnd  11161  fihashdom  11221  zfz1isolemiso  11269  cjap  11650  cvg1nlemcau  11728  cvg1nlemres  11729  resqrexlemlo  11757  resqrexlemcalc3  11760  absext  11807  xrnegiso  12006  xrminltinf  12016  fsumabs  12210  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  fprodle  12385  addmodlteqALT  12604  nn0seqcvgd  12797  algcvg  12804  algcvga  12807  eucalgcvga  12814  qnumgt0  12954  pcprendvds2  13048  pcpremul  13050  pcadd2  13098  2expltfac  13196  ctinfomlemom  13296  gzsumfzval  13688  mplsubgfilemcl  15013  ispsmet  15347  psmettri2  15352  ismet  15368  isxmet  15369  xmettri2  15385  blvalps  15412  blval  15413  comet  15523  bdxmet  15525  dvef  15751  cxplt  15941  rpcxple2  15943  rpcxplt2  15944  cxplt3  15945  apcxp2  15964  ltexp2  15966  logbleb  15986  logblt  15987  pellexlem3  16007  lgsdilem  16060  2lgslem1a2  16120  apdifflemr  17001  apdiff  17002