Theorem breq12d 4096

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 4088	. 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 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breq123d  4097  3brtr3d  4114  3brtr4d  4115  pocl  4394  csbcnvg  4906  cnvpom  5271  sbcfung  5342  isoeq1  5931  isocnv  5941  isotr  5946  caovordig  6177  caovordg  6179  caovord2d  6181  caovord  6183  ofrfval  6233  ofrval  6235  ofrfval2  6241  caofref  6249  fundmeng  6968  xpsneng  6989  xpcomeng  6995  xpdom2g  6999  phplem3g  7025  php5  7027  php5dom  7032  exmidpw2en  7085  exmidapne  7457  nqtri3or  7594  ltsonq  7596  ltanqg  7598  ltmnqg  7599  lt2addnq  7602  lt2mulnq  7603  prarloclemarch  7616  ltrnqg  7618  ltnnnq  7621  prarloclemlt  7691  addlocprlemgt  7732  mullocprlem  7768  addextpr  7819  recexprlemss1l  7833  recexprlemss1u  7834  recexpr  7836  caucvgprlemcanl  7842  cauappcvgprlemm  7843  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlemlim  7859  cauappcvgpr  7860  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgpr  7880  caucvgprprlemell  7883  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkeqj  7888  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexb  7905  caucvgprprlem1  7907  lttrsr  7960  ltposr  7961  ltsosr  7962  ltasrg  7968  aptisr  7977  mulextsr1lem  7978  mulextsr1  7979  caucvgsrlemcau  7991  caucvgsrlemgt1  7993  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  caucvgsr  8000  axpre-ltirr  8080  axpre-ltadd  8084  axpre-mulgt0  8085  axpre-mulext  8086  axcaucvglemcau  8096  axcaucvglemres  8097  ltadd2  8577  ltadd1  8587  leadd2  8589  reapval  8734  reapmul1  8753  remulext2  8758  apreim  8761  apirr  8763  apsym  8764  apcotr  8765  apadd1  8766  apadd2  8767  apneg  8769  mulext1  8770  mulext2  8771  apti  8780  apsub1  8800  subap0  8801  apmul1  8946  apmul2  8947  apdivmuld  8971  ltmul2  9014  lemul2  9015  ltdiv1  9026  ltdiv2  9045  ledivdiv  9048  lediv2  9049  negiso  9113  div4p1lem1div2  9376  qapne  9846  nn0ledivnn  9975  xleadd1  10083  xltadd1  10084  xltadd2  10085  xsubge0  10089  xleaddadd  10095  qtri3or  10472  frecfzennn  10660  monoord  10719  monoord2  10720  leexp1a  10828  bernneq  10894  apexp1  10952  nn0le2msqd  10953  faclbnd  10975  faclbnd3  10977  faclbnd6  10978  facubnd  10979  fihashdom  11037  zfz1isolemiso  11074  cjap  11433  cvg1nlemcau  11511  cvg1nlemres  11512  resqrexlemlo  11540  resqrexlemcalc3  11543  absext  11590  xrnegiso  11789  xrminltinf  11799  fsumabs  11992  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  fprodle  12167  addmodlteqALT  12386  nn0seqcvgd  12579  algcvg  12586  algcvga  12589  eucalgcvga  12596  qnumgt0  12736  pcprendvds2  12830  pcpremul  12832  pcadd2  12880  2expltfac  12978  ctinfomlemom  13014  gsumfzval  13440  mplsubgfilemcl  14679  ispsmet  15013  psmettri2  15018  ismet  15034  isxmet  15035  xmettri2  15051  blvalps  15078  blval  15079  comet  15189  bdxmet  15191  dvef  15417  cxplt  15606  rpcxple2  15608  rpcxplt2  15609  cxplt3  15610  apcxp2  15629  ltexp2  15631  logbleb  15651  logblt  15652  lgsdilem  15722  2lgslem1a2  15782  apdifflemr  16503  apdiff  16504