Theorem breq12d 4064

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	⊢ (𝜑 → 𝐴 = 𝐵)
breq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
breq12d	⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Proof of Theorem breq12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		breq12 4056	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   class class class wbr 4051

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 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-br 4052

This theorem is referenced by:  breq123d  4065  3brtr3d  4082  3brtr4d  4083  pocl  4358  csbcnvg  4870  cnvpom  5234  sbcfung  5304  isoeq1  5883  isocnv  5893  isotr  5898  caovordig  6125  caovordg  6127  caovord2d  6129  caovord  6131  ofrfval  6180  ofrval  6182  ofrfval2  6188  caofref  6196  fundmeng  6913  xpsneng  6932  xpcomeng  6938  xpdom2g  6942  phplem3g  6968  php5  6970  php5dom  6975  exmidpw2en  7024  exmidapne  7392  nqtri3or  7529  ltsonq  7531  ltanqg  7533  ltmnqg  7534  lt2addnq  7537  lt2mulnq  7538  prarloclemarch  7551  ltrnqg  7553  ltnnnq  7556  prarloclemlt  7626  addlocprlemgt  7667  mullocprlem  7703  addextpr  7754  recexprlemss1l  7768  recexprlemss1u  7769  recexpr  7771  caucvgprlemcanl  7777  cauappcvgprlemm  7778  cauappcvgprlemdisj  7784  cauappcvgprlemloc  7785  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  cauappcvgprlem1  7792  cauappcvgprlemlim  7794  cauappcvgpr  7795  caucvgprlemnkj  7799  caucvgprlemnbj  7800  caucvgprlemdisj  7807  caucvgprlemloc  7808  caucvgprlemcl  7809  caucvgprlemladdrl  7811  caucvgprlem1  7812  caucvgpr  7815  caucvgprprlemell  7818  caucvgprprlemcbv  7820  caucvgprprlemval  7821  caucvgprprlemnkeqj  7823  caucvgprprlemopl  7830  caucvgprprlemlol  7831  caucvgprprlemloc  7836  caucvgprprlemclphr  7838  caucvgprprlemexb  7840  caucvgprprlem1  7842  lttrsr  7895  ltposr  7896  ltsosr  7897  ltasrg  7903  aptisr  7912  mulextsr1lem  7913  mulextsr1  7914  caucvgsrlemcau  7926  caucvgsrlemgt1  7928  caucvgsrlemoffcau  7931  caucvgsrlemoffres  7933  caucvgsr  7935  axpre-ltirr  8015  axpre-ltadd  8019  axpre-mulgt0  8020  axpre-mulext  8021  axcaucvglemcau  8031  axcaucvglemres  8032  ltadd2  8512  ltadd1  8522  leadd2  8524  reapval  8669  reapmul1  8688  remulext2  8693  apreim  8696  apirr  8698  apsym  8699  apcotr  8700  apadd1  8701  apadd2  8702  apneg  8704  mulext1  8705  mulext2  8706  apti  8715  apsub1  8735  subap0  8736  apmul1  8881  apmul2  8882  apdivmuld  8906  ltmul2  8949  lemul2  8950  ltdiv1  8961  ltdiv2  8980  ledivdiv  8983  lediv2  8984  negiso  9048  div4p1lem1div2  9311  qapne  9780  nn0ledivnn  9909  xleadd1  10017  xltadd1  10018  xltadd2  10019  xsubge0  10023  xleaddadd  10029  qtri3or  10405  frecfzennn  10593  monoord  10652  monoord2  10653  leexp1a  10761  bernneq  10827  apexp1  10885  nn0le2msqd  10886  faclbnd  10908  faclbnd3  10910  faclbnd6  10911  facubnd  10912  fihashdom  10970  zfz1isolemiso  11006  cjap  11292  cvg1nlemcau  11370  cvg1nlemres  11371  resqrexlemlo  11399  resqrexlemcalc3  11402  absext  11449  xrnegiso  11648  xrminltinf  11658  fsumabs  11851  cvgratnnlemnexp  11910  cvgratnnlemmn  11911  fprodle  12026  addmodlteqALT  12245  nn0seqcvgd  12438  algcvg  12445  algcvga  12448  eucalgcvga  12455  qnumgt0  12595  pcprendvds2  12689  pcpremul  12691  pcadd2  12739  2expltfac  12837  ctinfomlemom  12873  gsumfzval  13298  mplsubgfilemcl  14536  ispsmet  14870  psmettri2  14875  ismet  14891  isxmet  14892  xmettri2  14908  blvalps  14935  blval  14936  comet  15046  bdxmet  15048  dvef  15274  cxplt  15463  rpcxple2  15465  rpcxplt2  15466  cxplt3  15467  apcxp2  15486  ltexp2  15488  logbleb  15508  logblt  15509  lgsdilem  15579  2lgslem1a2  15639  apdifflemr  16127  apdiff  16128