Theorem breq12d 3942

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1331   class class class wbr 3929

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930

This theorem is referenced by:  breq123d  3943  3brtr3d  3959  3brtr4d  3960  pocl  4225  csbcnvg  4723  cnvpom  5081  sbcfung  5147  isoeq1  5702  isocnv  5712  isotr  5717  caovordig  5936  caovordg  5938  caovord2d  5940  caovord  5942  ofrfval  5990  ofrval  5992  ofrfval2  5998  caofref  6003  fundmeng  6701  xpsneng  6716  xpcomeng  6722  xpdom2g  6726  phplem3g  6750  php5  6752  php5dom  6757  nqtri3or  7204  ltsonq  7206  ltanqg  7208  ltmnqg  7209  lt2addnq  7212  lt2mulnq  7213  prarloclemarch  7226  ltrnqg  7228  ltnnnq  7231  prarloclemlt  7301  addlocprlemgt  7342  mullocprlem  7378  addextpr  7429  recexprlemss1l  7443  recexprlemss1u  7444  recexpr  7446  caucvgprlemcanl  7452  cauappcvgprlemm  7453  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem1  7467  cauappcvgprlemlim  7469  cauappcvgpr  7470  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemcl  7484  caucvgprlemladdrl  7486  caucvgprlem1  7487  caucvgpr  7490  caucvgprprlemell  7493  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemnkeqj  7498  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemloc  7511  caucvgprprlemclphr  7513  caucvgprprlemexb  7515  caucvgprprlem1  7517  lttrsr  7570  ltposr  7571  ltsosr  7572  ltasrg  7578  aptisr  7587  mulextsr1lem  7588  mulextsr1  7589  caucvgsrlemcau  7601  caucvgsrlemgt1  7603  caucvgsrlemoffcau  7606  caucvgsrlemoffres  7608  caucvgsr  7610  axpre-ltirr  7690  axpre-ltadd  7694  axpre-mulgt0  7695  axpre-mulext  7696  axcaucvglemcau  7706  axcaucvglemres  7707  ltadd2  8181  ltadd1  8191  leadd2  8193  reapval  8338  reapmul1  8357  remulext2  8362  apreim  8365  apirr  8367  apsym  8368  apcotr  8369  apadd1  8370  apadd2  8371  apneg  8373  mulext1  8374  mulext2  8375  apti  8384  apsub1  8404  subap0  8405  apmul1  8548  apmul2  8549  apdivmuld  8573  ltmul2  8614  lemul2  8615  ltdiv1  8626  ltdiv2  8645  ledivdiv  8648  lediv2  8649  negiso  8713  div4p1lem1div2  8973  qapne  9431  nn0ledivnn  9554  xleadd1  9658  xltadd1  9659  xltadd2  9660  xsubge0  9664  xleaddadd  9670  qtri3or  10020  frecfzennn  10199  monoord  10249  monoord2  10250  leexp1a  10348  bernneq  10412  nn0le2msqd  10465  faclbnd  10487  faclbnd3  10489  faclbnd6  10490  facubnd  10491  fihashdom  10549  zfz1isolemiso  10582  cjap  10678  cvg1nlemcau  10756  cvg1nlemres  10757  resqrexlemlo  10785  resqrexlemcalc3  10788  absext  10835  xrnegiso  11031  xrminltinf  11041  fsumabs  11234  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  addmodlteqALT  11557  nn0seqcvgd  11722  algcvg  11729  algcvga  11732  eucalgcvga  11739  qnumgt0  11876  ctinfomlemom  11940  ispsmet  12492  psmettri2  12497  ismet  12513  isxmet  12514  xmettri2  12530  blvalps  12557  blval  12558  comet  12668  bdxmet  12670  dvef  12856