Theorem breq12d 4058

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 4050	. 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 1373   class class class wbr 4045

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046

This theorem is referenced by:  breq123d  4059  3brtr3d  4076  3brtr4d  4077  pocl  4351  csbcnvg  4863  cnvpom  5226  sbcfung  5296  isoeq1  5872  isocnv  5882  isotr  5887  caovordig  6114  caovordg  6116  caovord2d  6118  caovord  6120  ofrfval  6169  ofrval  6171  ofrfval2  6177  caofref  6185  fundmeng  6901  xpsneng  6919  xpcomeng  6925  xpdom2g  6929  phplem3g  6955  php5  6957  php5dom  6962  exmidpw2en  7011  exmidapne  7374  nqtri3or  7511  ltsonq  7513  ltanqg  7515  ltmnqg  7516  lt2addnq  7519  lt2mulnq  7520  prarloclemarch  7533  ltrnqg  7535  ltnnnq  7538  prarloclemlt  7608  addlocprlemgt  7649  mullocprlem  7685  addextpr  7736  recexprlemss1l  7750  recexprlemss1u  7751  recexpr  7753  caucvgprlemcanl  7759  cauappcvgprlemm  7760  cauappcvgprlemdisj  7766  cauappcvgprlemloc  7767  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  cauappcvgprlemlim  7776  cauappcvgpr  7777  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemcl  7791  caucvgprlemladdrl  7793  caucvgprlem1  7794  caucvgpr  7797  caucvgprprlemell  7800  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemnkeqj  7805  caucvgprprlemopl  7812  caucvgprprlemlol  7813  caucvgprprlemloc  7818  caucvgprprlemclphr  7820  caucvgprprlemexb  7822  caucvgprprlem1  7824  lttrsr  7877  ltposr  7878  ltsosr  7879  ltasrg  7885  aptisr  7894  mulextsr1lem  7895  mulextsr1  7896  caucvgsrlemcau  7908  caucvgsrlemgt1  7910  caucvgsrlemoffcau  7913  caucvgsrlemoffres  7915  caucvgsr  7917  axpre-ltirr  7997  axpre-ltadd  8001  axpre-mulgt0  8002  axpre-mulext  8003  axcaucvglemcau  8013  axcaucvglemres  8014  ltadd2  8494  ltadd1  8504  leadd2  8506  reapval  8651  reapmul1  8670  remulext2  8675  apreim  8678  apirr  8680  apsym  8681  apcotr  8682  apadd1  8683  apadd2  8684  apneg  8686  mulext1  8687  mulext2  8688  apti  8697  apsub1  8717  subap0  8718  apmul1  8863  apmul2  8864  apdivmuld  8888  ltmul2  8931  lemul2  8932  ltdiv1  8943  ltdiv2  8962  ledivdiv  8965  lediv2  8966  negiso  9030  div4p1lem1div2  9293  qapne  9762  nn0ledivnn  9891  xleadd1  9999  xltadd1  10000  xltadd2  10001  xsubge0  10005  xleaddadd  10011  qtri3or  10385  frecfzennn  10573  monoord  10632  monoord2  10633  leexp1a  10741  bernneq  10807  apexp1  10865  nn0le2msqd  10866  faclbnd  10888  faclbnd3  10890  faclbnd6  10891  facubnd  10892  fihashdom  10950  zfz1isolemiso  10986  cjap  11250  cvg1nlemcau  11328  cvg1nlemres  11329  resqrexlemlo  11357  resqrexlemcalc3  11360  absext  11407  xrnegiso  11606  xrminltinf  11616  fsumabs  11809  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  fprodle  11984  addmodlteqALT  12203  nn0seqcvgd  12396  algcvg  12403  algcvga  12406  eucalgcvga  12413  qnumgt0  12553  pcprendvds2  12647  pcpremul  12649  pcadd2  12697  2expltfac  12795  ctinfomlemom  12831  gsumfzval  13256  mplsubgfilemcl  14494  ispsmet  14828  psmettri2  14833  ismet  14849  isxmet  14850  xmettri2  14866  blvalps  14893  blval  14894  comet  15004  bdxmet  15006  dvef  15232  cxplt  15421  rpcxple2  15423  rpcxplt2  15424  cxplt3  15425  apcxp2  15444  ltexp2  15446  logbleb  15466  logblt  15467  lgsdilem  15537  2lgslem1a2  15597  apdifflemr  16023  apdiff  16024