Theorem breq12d 4002

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 3994	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2anc 409	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348   class class class wbr 3989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990

This theorem is referenced by:  breq123d  4003  3brtr3d  4020  3brtr4d  4021  pocl  4288  csbcnvg  4795  cnvpom  5153  sbcfung  5222  isoeq1  5780  isocnv  5790  isotr  5795  caovordig  6018  caovordg  6020  caovord2d  6022  caovord  6024  ofrfval  6069  ofrval  6071  ofrfval2  6077  caofref  6082  fundmeng  6785  xpsneng  6800  xpcomeng  6806  xpdom2g  6810  phplem3g  6834  php5  6836  php5dom  6841  nqtri3or  7358  ltsonq  7360  ltanqg  7362  ltmnqg  7363  lt2addnq  7366  lt2mulnq  7367  prarloclemarch  7380  ltrnqg  7382  ltnnnq  7385  prarloclemlt  7455  addlocprlemgt  7496  mullocprlem  7532  addextpr  7583  recexprlemss1l  7597  recexprlemss1u  7598  recexpr  7600  caucvgprlemcanl  7606  cauappcvgprlemm  7607  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlemlim  7623  cauappcvgpr  7624  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemcl  7638  caucvgprlemladdrl  7640  caucvgprlem1  7641  caucvgpr  7644  caucvgprprlemell  7647  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemnkeqj  7652  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemloc  7665  caucvgprprlemclphr  7667  caucvgprprlemexb  7669  caucvgprprlem1  7671  lttrsr  7724  ltposr  7725  ltsosr  7726  ltasrg  7732  aptisr  7741  mulextsr1lem  7742  mulextsr1  7743  caucvgsrlemcau  7755  caucvgsrlemgt1  7757  caucvgsrlemoffcau  7760  caucvgsrlemoffres  7762  caucvgsr  7764  axpre-ltirr  7844  axpre-ltadd  7848  axpre-mulgt0  7849  axpre-mulext  7850  axcaucvglemcau  7860  axcaucvglemres  7861  ltadd2  8338  ltadd1  8348  leadd2  8350  reapval  8495  reapmul1  8514  remulext2  8519  apreim  8522  apirr  8524  apsym  8525  apcotr  8526  apadd1  8527  apadd2  8528  apneg  8530  mulext1  8531  mulext2  8532  apti  8541  apsub1  8561  subap0  8562  apmul1  8705  apmul2  8706  apdivmuld  8730  ltmul2  8772  lemul2  8773  ltdiv1  8784  ltdiv2  8803  ledivdiv  8806  lediv2  8807  negiso  8871  div4p1lem1div2  9131  qapne  9598  nn0ledivnn  9724  xleadd1  9832  xltadd1  9833  xltadd2  9834  xsubge0  9838  xleaddadd  9844  qtri3or  10199  frecfzennn  10382  monoord  10432  monoord2  10433  leexp1a  10531  bernneq  10596  apexp1  10652  nn0le2msqd  10653  faclbnd  10675  faclbnd3  10677  faclbnd6  10678  facubnd  10679  fihashdom  10738  zfz1isolemiso  10774  cjap  10870  cvg1nlemcau  10948  cvg1nlemres  10949  resqrexlemlo  10977  resqrexlemcalc3  10980  absext  11027  xrnegiso  11225  xrminltinf  11235  fsumabs  11428  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  fprodle  11603  addmodlteqALT  11819  nn0seqcvgd  11995  algcvg  12002  algcvga  12005  eucalgcvga  12012  qnumgt0  12152  pcprendvds2  12245  pcpremul  12247  ctinfomlemom  12382  ispsmet  13117  psmettri2  13122  ismet  13138  isxmet  13139  xmettri2  13155  blvalps  13182  blval  13183  comet  13293  bdxmet  13295  dvef  13482  cxplt  13630  rpcxple2  13632  rpcxplt2  13633  cxplt3  13634  apcxp2  13652  ltexp2  13654  logbleb  13673  logblt  13674  lgsdilem  13722  apdifflemr  14079  apdiff  14080