Theorem breq12d 4031

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 4023	. 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 4018

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-br 4019

This theorem is referenced by:  breq123d  4032  3brtr3d  4049  3brtr4d  4050  pocl  4321  csbcnvg  4829  cnvpom  5189  sbcfung  5259  isoeq1  5823  isocnv  5833  isotr  5838  caovordig  6063  caovordg  6065  caovord2d  6067  caovord  6069  ofrfval  6116  ofrval  6118  ofrfval2  6124  caofref  6129  fundmeng  6834  xpsneng  6849  xpcomeng  6855  xpdom2g  6859  phplem3g  6885  php5  6887  php5dom  6892  exmidpw2en  6941  exmidapne  7290  nqtri3or  7426  ltsonq  7428  ltanqg  7430  ltmnqg  7431  lt2addnq  7434  lt2mulnq  7435  prarloclemarch  7448  ltrnqg  7450  ltnnnq  7453  prarloclemlt  7523  addlocprlemgt  7564  mullocprlem  7600  addextpr  7651  recexprlemss1l  7665  recexprlemss1u  7666  recexpr  7668  caucvgprlemcanl  7674  cauappcvgprlemm  7675  cauappcvgprlemdisj  7681  cauappcvgprlemloc  7682  cauappcvgprlemladdru  7686  cauappcvgprlemladdrl  7687  cauappcvgprlem1  7689  cauappcvgprlemlim  7691  cauappcvgpr  7692  caucvgprlemnkj  7696  caucvgprlemnbj  7697  caucvgprlemdisj  7704  caucvgprlemloc  7705  caucvgprlemcl  7706  caucvgprlemladdrl  7708  caucvgprlem1  7709  caucvgpr  7712  caucvgprprlemell  7715  caucvgprprlemcbv  7717  caucvgprprlemval  7718  caucvgprprlemnkeqj  7720  caucvgprprlemopl  7727  caucvgprprlemlol  7728  caucvgprprlemloc  7733  caucvgprprlemclphr  7735  caucvgprprlemexb  7737  caucvgprprlem1  7739  lttrsr  7792  ltposr  7793  ltsosr  7794  ltasrg  7800  aptisr  7809  mulextsr1lem  7810  mulextsr1  7811  caucvgsrlemcau  7823  caucvgsrlemgt1  7825  caucvgsrlemoffcau  7828  caucvgsrlemoffres  7830  caucvgsr  7832  axpre-ltirr  7912  axpre-ltadd  7916  axpre-mulgt0  7917  axpre-mulext  7918  axcaucvglemcau  7928  axcaucvglemres  7929  ltadd2  8407  ltadd1  8417  leadd2  8419  reapval  8564  reapmul1  8583  remulext2  8588  apreim  8591  apirr  8593  apsym  8594  apcotr  8595  apadd1  8596  apadd2  8597  apneg  8599  mulext1  8600  mulext2  8601  apti  8610  apsub1  8630  subap0  8631  apmul1  8776  apmul2  8777  apdivmuld  8801  ltmul2  8844  lemul2  8845  ltdiv1  8856  ltdiv2  8875  ledivdiv  8878  lediv2  8879  negiso  8943  div4p1lem1div2  9203  qapne  9671  nn0ledivnn  9799  xleadd1  9907  xltadd1  9908  xltadd2  9909  xsubge0  9913  xleaddadd  9919  qtri3or  10275  frecfzennn  10459  monoord  10509  monoord2  10510  leexp1a  10609  bernneq  10675  apexp1  10733  nn0le2msqd  10734  faclbnd  10756  faclbnd3  10758  faclbnd6  10759  facubnd  10760  fihashdom  10818  zfz1isolemiso  10854  cjap  10950  cvg1nlemcau  11028  cvg1nlemres  11029  resqrexlemlo  11057  resqrexlemcalc3  11060  absext  11107  xrnegiso  11305  xrminltinf  11315  fsumabs  11508  cvgratnnlemnexp  11567  cvgratnnlemmn  11568  fprodle  11683  addmodlteqALT  11900  nn0seqcvgd  12076  algcvg  12083  algcvga  12086  eucalgcvga  12093  qnumgt0  12233  pcprendvds2  12326  pcpremul  12328  pcadd2  12376  ctinfomlemom  12481  ispsmet  14300  psmettri2  14305  ismet  14321  isxmet  14322  xmettri2  14338  blvalps  14365  blval  14366  comet  14476  bdxmet  14478  dvef  14665  cxplt  14813  rpcxple2  14815  rpcxplt2  14816  cxplt3  14817  apcxp2  14835  ltexp2  14837  logbleb  14856  logblt  14857  lgsdilem  14906  apdifflemr  15274  apdiff  15275