Theorem breq12d 4106

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  breq123d  4107  3brtr3d  4124  3brtr4d  4125  pocl  4406  csbcnvg  4920  cnvpom  5286  sbcfung  5357  isoeq1  5952  isocnv  5962  isotr  5967  caovordig  6198  caovordg  6200  caovord2d  6202  caovord  6204  ofrfval  6253  ofrval  6255  ofrfval2  6261  caofref  6269  fundmeng  7025  xpsneng  7049  xpcomeng  7055  xpdom2g  7059  phplem3g  7085  php5  7087  php5dom  7092  exmidpw2en  7147  exmidapne  7522  nqtri3or  7659  ltsonq  7661  ltanqg  7663  ltmnqg  7664  lt2addnq  7667  lt2mulnq  7668  prarloclemarch  7681  ltrnqg  7683  ltnnnq  7686  prarloclemlt  7756  addlocprlemgt  7797  mullocprlem  7833  addextpr  7884  recexprlemss1l  7898  recexprlemss1u  7899  recexpr  7901  caucvgprlemcanl  7907  cauappcvgprlemm  7908  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem1  7922  cauappcvgprlemlim  7924  cauappcvgpr  7925  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdrl  7941  caucvgprlem1  7942  caucvgpr  7945  caucvgprprlemell  7948  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemnkeqj  7953  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemloc  7966  caucvgprprlemclphr  7968  caucvgprprlemexb  7970  caucvgprprlem1  7972  lttrsr  8025  ltposr  8026  ltsosr  8027  ltasrg  8033  aptisr  8042  mulextsr1lem  8043  mulextsr1  8044  caucvgsrlemcau  8056  caucvgsrlemgt1  8058  caucvgsrlemoffcau  8061  caucvgsrlemoffres  8063  caucvgsr  8065  axpre-ltirr  8145  axpre-ltadd  8149  axpre-mulgt0  8150  axpre-mulext  8151  axcaucvglemcau  8161  axcaucvglemres  8162  ltadd2  8641  ltadd1  8651  leadd2  8653  reapval  8798  reapmul1  8817  remulext2  8822  apreim  8825  apirr  8827  apsym  8828  apcotr  8829  apadd1  8830  apadd2  8831  apneg  8833  mulext1  8834  mulext2  8835  apti  8844  apsub1  8864  subap0  8865  apmul1  9010  apmul2  9011  apdivmuld  9035  ltmul2  9078  lemul2  9079  ltdiv1  9090  ltdiv2  9109  ledivdiv  9112  lediv2  9113  negiso  9177  div4p1lem1div2  9440  qapne  9917  nn0ledivnn  10046  xleadd1  10154  xltadd1  10155  xltadd2  10156  xsubge0  10160  xleaddadd  10166  qtri3or  10546  frecfzennn  10734  monoord  10793  monoord2  10794  leexp1a  10902  bernneq  10968  apexp1  11026  nn0le2msqd  11027  faclbnd  11049  faclbnd3  11051  faclbnd6  11052  facubnd  11053  fihashdom  11112  zfz1isolemiso  11149  cjap  11529  cvg1nlemcau  11607  cvg1nlemres  11608  resqrexlemlo  11636  resqrexlemcalc3  11639  absext  11686  xrnegiso  11885  xrminltinf  11895  fsumabs  12089  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  fprodle  12264  addmodlteqALT  12483  nn0seqcvgd  12676  algcvg  12683  algcvga  12686  eucalgcvga  12693  qnumgt0  12833  pcprendvds2  12927  pcpremul  12929  pcadd2  12977  2expltfac  13075  ctinfomlemom  13111  gsumfzval  13537  mplsubgfilemcl  14783  ispsmet  15117  psmettri2  15122  ismet  15138  isxmet  15139  xmettri2  15155  blvalps  15182  blval  15183  comet  15293  bdxmet  15295  dvef  15521  cxplt  15710  rpcxple2  15712  rpcxplt2  15713  cxplt3  15714  apcxp2  15733  ltexp2  15735  logbleb  15755  logblt  15756  pellexlem3  15776  lgsdilem  15829  2lgslem1a2  15889  apdifflemr  16762  apdiff  16763