Theorem breq12d 4072

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 4064	. 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 4059

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060

This theorem is referenced by:  breq123d  4073  3brtr3d  4090  3brtr4d  4091  pocl  4368  csbcnvg  4880  cnvpom  5244  sbcfung  5314  isoeq1  5893  isocnv  5903  isotr  5908  caovordig  6135  caovordg  6137  caovord2d  6139  caovord  6141  ofrfval  6190  ofrval  6192  ofrfval2  6198  caofref  6206  fundmeng  6923  xpsneng  6942  xpcomeng  6948  xpdom2g  6952  phplem3g  6978  php5  6980  php5dom  6985  exmidpw2en  7035  exmidapne  7407  nqtri3or  7544  ltsonq  7546  ltanqg  7548  ltmnqg  7549  lt2addnq  7552  lt2mulnq  7553  prarloclemarch  7566  ltrnqg  7568  ltnnnq  7571  prarloclemlt  7641  addlocprlemgt  7682  mullocprlem  7718  addextpr  7769  recexprlemss1l  7783  recexprlemss1u  7784  recexpr  7786  caucvgprlemcanl  7792  cauappcvgprlemm  7793  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  cauappcvgprlemlim  7809  cauappcvgpr  7810  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemcl  7824  caucvgprlemladdrl  7826  caucvgprlem1  7827  caucvgpr  7830  caucvgprprlemell  7833  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemnkeqj  7838  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemloc  7851  caucvgprprlemclphr  7853  caucvgprprlemexb  7855  caucvgprprlem1  7857  lttrsr  7910  ltposr  7911  ltsosr  7912  ltasrg  7918  aptisr  7927  mulextsr1lem  7928  mulextsr1  7929  caucvgsrlemcau  7941  caucvgsrlemgt1  7943  caucvgsrlemoffcau  7946  caucvgsrlemoffres  7948  caucvgsr  7950  axpre-ltirr  8030  axpre-ltadd  8034  axpre-mulgt0  8035  axpre-mulext  8036  axcaucvglemcau  8046  axcaucvglemres  8047  ltadd2  8527  ltadd1  8537  leadd2  8539  reapval  8684  reapmul1  8703  remulext2  8708  apreim  8711  apirr  8713  apsym  8714  apcotr  8715  apadd1  8716  apadd2  8717  apneg  8719  mulext1  8720  mulext2  8721  apti  8730  apsub1  8750  subap0  8751  apmul1  8896  apmul2  8897  apdivmuld  8921  ltmul2  8964  lemul2  8965  ltdiv1  8976  ltdiv2  8995  ledivdiv  8998  lediv2  8999  negiso  9063  div4p1lem1div2  9326  qapne  9795  nn0ledivnn  9924  xleadd1  10032  xltadd1  10033  xltadd2  10034  xsubge0  10038  xleaddadd  10044  qtri3or  10420  frecfzennn  10608  monoord  10667  monoord2  10668  leexp1a  10776  bernneq  10842  apexp1  10900  nn0le2msqd  10901  faclbnd  10923  faclbnd3  10925  faclbnd6  10926  facubnd  10927  fihashdom  10985  zfz1isolemiso  11021  cjap  11332  cvg1nlemcau  11410  cvg1nlemres  11411  resqrexlemlo  11439  resqrexlemcalc3  11442  absext  11489  xrnegiso  11688  xrminltinf  11698  fsumabs  11891  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  fprodle  12066  addmodlteqALT  12285  nn0seqcvgd  12478  algcvg  12485  algcvga  12488  eucalgcvga  12495  qnumgt0  12635  pcprendvds2  12729  pcpremul  12731  pcadd2  12779  2expltfac  12877  ctinfomlemom  12913  gsumfzval  13338  mplsubgfilemcl  14576  ispsmet  14910  psmettri2  14915  ismet  14931  isxmet  14932  xmettri2  14948  blvalps  14975  blval  14976  comet  15086  bdxmet  15088  dvef  15314  cxplt  15503  rpcxple2  15505  rpcxplt2  15506  cxplt3  15507  apcxp2  15526  ltexp2  15528  logbleb  15548  logblt  15549  lgsdilem  15619  2lgslem1a2  15679  apdifflemr  16188  apdiff  16189