Theorem breq12d 4046

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 4038	. 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 1364   class class class wbr 4033

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034

This theorem is referenced by:  breq123d  4047  3brtr3d  4064  3brtr4d  4065  pocl  4338  csbcnvg  4850  cnvpom  5212  sbcfung  5282  isoeq1  5848  isocnv  5858  isotr  5863  caovordig  6089  caovordg  6091  caovord2d  6093  caovord  6095  ofrfval  6144  ofrval  6146  ofrfval2  6152  caofref  6159  fundmeng  6866  xpsneng  6881  xpcomeng  6887  xpdom2g  6891  phplem3g  6917  php5  6919  php5dom  6924  exmidpw2en  6973  exmidapne  7327  nqtri3or  7463  ltsonq  7465  ltanqg  7467  ltmnqg  7468  lt2addnq  7471  lt2mulnq  7472  prarloclemarch  7485  ltrnqg  7487  ltnnnq  7490  prarloclemlt  7560  addlocprlemgt  7601  mullocprlem  7637  addextpr  7688  recexprlemss1l  7702  recexprlemss1u  7703  recexpr  7705  caucvgprlemcanl  7711  cauappcvgprlemm  7712  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  cauappcvgprlemlim  7728  cauappcvgpr  7729  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemcl  7743  caucvgprlemladdrl  7745  caucvgprlem1  7746  caucvgpr  7749  caucvgprprlemell  7752  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemnkeqj  7757  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemloc  7770  caucvgprprlemclphr  7772  caucvgprprlemexb  7774  caucvgprprlem1  7776  lttrsr  7829  ltposr  7830  ltsosr  7831  ltasrg  7837  aptisr  7846  mulextsr1lem  7847  mulextsr1  7848  caucvgsrlemcau  7860  caucvgsrlemgt1  7862  caucvgsrlemoffcau  7865  caucvgsrlemoffres  7867  caucvgsr  7869  axpre-ltirr  7949  axpre-ltadd  7953  axpre-mulgt0  7954  axpre-mulext  7955  axcaucvglemcau  7965  axcaucvglemres  7966  ltadd2  8446  ltadd1  8456  leadd2  8458  reapval  8603  reapmul1  8622  remulext2  8627  apreim  8630  apirr  8632  apsym  8633  apcotr  8634  apadd1  8635  apadd2  8636  apneg  8638  mulext1  8639  mulext2  8640  apti  8649  apsub1  8669  subap0  8670  apmul1  8815  apmul2  8816  apdivmuld  8840  ltmul2  8883  lemul2  8884  ltdiv1  8895  ltdiv2  8914  ledivdiv  8917  lediv2  8918  negiso  8982  div4p1lem1div2  9245  qapne  9713  nn0ledivnn  9842  xleadd1  9950  xltadd1  9951  xltadd2  9952  xsubge0  9956  xleaddadd  9962  qtri3or  10330  frecfzennn  10518  monoord  10577  monoord2  10578  leexp1a  10686  bernneq  10752  apexp1  10810  nn0le2msqd  10811  faclbnd  10833  faclbnd3  10835  faclbnd6  10836  facubnd  10837  fihashdom  10895  zfz1isolemiso  10931  cjap  11071  cvg1nlemcau  11149  cvg1nlemres  11150  resqrexlemlo  11178  resqrexlemcalc3  11181  absext  11228  xrnegiso  11427  xrminltinf  11437  fsumabs  11630  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  fprodle  11805  addmodlteqALT  12024  nn0seqcvgd  12209  algcvg  12216  algcvga  12219  eucalgcvga  12226  qnumgt0  12366  pcprendvds2  12460  pcpremul  12462  pcadd2  12510  2expltfac  12608  ctinfomlemom  12644  gsumfzval  13034  ispsmet  14559  psmettri2  14564  ismet  14580  isxmet  14581  xmettri2  14597  blvalps  14624  blval  14625  comet  14735  bdxmet  14737  dvef  14963  cxplt  15152  rpcxple2  15154  rpcxplt2  15155  cxplt3  15156  apcxp2  15175  ltexp2  15177  logbleb  15197  logblt  15198  lgsdilem  15268  2lgslem1a2  15328  apdifflemr  15691  apdiff  15692