Theorem breq12d 4017

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 4009	. 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 1353   class class class wbr 4004

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005

This theorem is referenced by:  breq123d  4018  3brtr3d  4035  3brtr4d  4036  pocl  4304  csbcnvg  4812  cnvpom  5172  sbcfung  5241  isoeq1  5802  isocnv  5812  isotr  5817  caovordig  6040  caovordg  6042  caovord2d  6044  caovord  6046  ofrfval  6091  ofrval  6093  ofrfval2  6099  caofref  6104  fundmeng  6807  xpsneng  6822  xpcomeng  6828  xpdom2g  6832  phplem3g  6856  php5  6858  php5dom  6863  exmidapne  7259  nqtri3or  7395  ltsonq  7397  ltanqg  7399  ltmnqg  7400  lt2addnq  7403  lt2mulnq  7404  prarloclemarch  7417  ltrnqg  7419  ltnnnq  7422  prarloclemlt  7492  addlocprlemgt  7533  mullocprlem  7569  addextpr  7620  recexprlemss1l  7634  recexprlemss1u  7635  recexpr  7637  caucvgprlemcanl  7643  cauappcvgprlemm  7644  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  cauappcvgprlemlim  7660  cauappcvgpr  7661  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemcl  7675  caucvgprlemladdrl  7677  caucvgprlem1  7678  caucvgpr  7681  caucvgprprlemell  7684  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemnkeqj  7689  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemloc  7702  caucvgprprlemclphr  7704  caucvgprprlemexb  7706  caucvgprprlem1  7708  lttrsr  7761  ltposr  7762  ltsosr  7763  ltasrg  7769  aptisr  7778  mulextsr1lem  7779  mulextsr1  7780  caucvgsrlemcau  7792  caucvgsrlemgt1  7794  caucvgsrlemoffcau  7797  caucvgsrlemoffres  7799  caucvgsr  7801  axpre-ltirr  7881  axpre-ltadd  7885  axpre-mulgt0  7886  axpre-mulext  7887  axcaucvglemcau  7897  axcaucvglemres  7898  ltadd2  8376  ltadd1  8386  leadd2  8388  reapval  8533  reapmul1  8552  remulext2  8557  apreim  8560  apirr  8562  apsym  8563  apcotr  8564  apadd1  8565  apadd2  8566  apneg  8568  mulext1  8569  mulext2  8570  apti  8579  apsub1  8599  subap0  8600  apmul1  8745  apmul2  8746  apdivmuld  8770  ltmul2  8813  lemul2  8814  ltdiv1  8825  ltdiv2  8844  ledivdiv  8847  lediv2  8848  negiso  8912  div4p1lem1div2  9172  qapne  9639  nn0ledivnn  9767  xleadd1  9875  xltadd1  9876  xltadd2  9877  xsubge0  9881  xleaddadd  9887  qtri3or  10243  frecfzennn  10426  monoord  10476  monoord2  10477  leexp1a  10575  bernneq  10641  apexp1  10698  nn0le2msqd  10699  faclbnd  10721  faclbnd3  10723  faclbnd6  10724  facubnd  10725  fihashdom  10783  zfz1isolemiso  10819  cjap  10915  cvg1nlemcau  10993  cvg1nlemres  10994  resqrexlemlo  11022  resqrexlemcalc3  11025  absext  11072  xrnegiso  11270  xrminltinf  11280  fsumabs  11473  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  fprodle  11648  addmodlteqALT  11865  nn0seqcvgd  12041  algcvg  12048  algcvga  12051  eucalgcvga  12058  qnumgt0  12198  pcprendvds2  12291  pcpremul  12293  ctinfomlemom  12428  ispsmet  13826  psmettri2  13831  ismet  13847  isxmet  13848  xmettri2  13864  blvalps  13891  blval  13892  comet  14002  bdxmet  14004  dvef  14191  cxplt  14339  rpcxple2  14341  rpcxplt2  14342  cxplt3  14343  apcxp2  14361  ltexp2  14363  logbleb  14382  logblt  14383  lgsdilem  14431  apdifflemr  14798  apdiff  14799