Theorem breq12d 3798

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

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1284   class class class wbr 3785

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-br 3786

This theorem is referenced by:  breq123d  3799  3brtr3d  3814  3brtr4d  3815  pocl  4058  csbcnvg  4537  cnvpom  4880  sbcfung  4945  isoeq1  5461  isocnv  5471  isotr  5476  caovordig  5686  caovordg  5688  caovord2d  5690  caovord  5692  ofrfval  5740  ofrval  5742  ofrfval2  5747  caofref  5752  fundmeng  6310  xpsneng  6319  xpcomeng  6325  xpdom2g  6329  phplem3g  6342  php5  6344  php5dom  6349  nqtri3or  6586  ltsonq  6588  ltanqg  6590  ltmnqg  6591  lt2addnq  6594  lt2mulnq  6595  prarloclemarch  6608  ltrnqg  6610  ltnnnq  6613  prarloclemlt  6683  addlocprlemgt  6724  mullocprlem  6760  addextpr  6811  recexprlemss1l  6825  recexprlemss1u  6826  recexpr  6828  caucvgprlemcanl  6834  cauappcvgprlemm  6835  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  cauappcvgprlemlim  6851  cauappcvgpr  6852  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemcl  6866  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgpr  6872  caucvgprprlemell  6875  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemnkeqj  6880  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemloc  6893  caucvgprprlemclphr  6895  caucvgprprlemexb  6897  caucvgprprlem1  6899  lttrsr  6939  ltposr  6940  ltsosr  6941  ltasrg  6947  aptisr  6955  mulextsr1lem  6956  mulextsr1  6957  caucvgsrlemcau  6969  caucvgsrlemgt1  6971  caucvgsrlemoffcau  6974  caucvgsrlemoffres  6976  caucvgsr  6978  axpre-ltirr  7048  axpre-ltadd  7052  axpre-mulgt0  7053  axpre-mulext  7054  axcaucvglemcau  7064  axcaucvglemres  7065  ltadd2  7523  ltadd1  7533  leadd2  7535  reapval  7676  reapmul1  7695  remulext2  7700  apreim  7703  apirr  7705  apsym  7706  apcotr  7707  apadd1  7708  apadd2  7709  apneg  7711  mulext1  7712  mulext2  7713  apti  7722  apmul1  7876  ltmul2  7934  lemul2  7935  ltdiv1  7946  ltdiv2  7965  ledivdiv  7968  lediv2  7969  negiso  8033  div4p1lem1div2  8284  qapne  8724  nn0ledivnn  8838  qtri3or  9252  frecfzennn  9419  monoord  9455  monoord2  9456  leexp1a  9531  bernneq  9593  nn0le2msqd  9646  faclbnd  9668  faclbnd3  9670  faclbnd6  9671  facubnd  9672  cjap  9793  cvg1nlemcau  9870  cvg1nlemres  9871  resqrexlemlo  9899  resqrexlemcalc3  9902  absext  9949  addmodlteqALT  10259  nn0seqcvgd  10423  ialgcvg  10430  ialgcvga  10433  eucialgcvga  10440