Theorem breq12d 3747

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	⊢ (φ → A = B)
breq12d.2	⊢ (φ → 𝐶 = 𝐷)

Assertion

Ref	Expression
breq12d	⊢ (φ → (A𝑅𝐶 ↔ B𝑅𝐷))

Proof of Theorem breq12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (φ → A = B)
2		breq12d.2	. 2 ⊢ (φ → 𝐶 = 𝐷)
3		breq12 3739	. 2 ⊢ ((A = B ∧ 𝐶 = 𝐷) → (A𝑅𝐶 ↔ B𝑅𝐷))
4	1, 2, 3	syl2anc 393	1 ⊢ (φ → (A𝑅𝐶 ↔ B𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1226   class class class wbr 3734

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-un 2895  df-sn 3352  df-pr 3353  df-op 3355  df-br 3735

This theorem is referenced by:  breq123d  3748  3brtr3d  3763  3brtr4d  3764  pocl  4010  csbcnvg  4442  cnvpom  4783  sbcfung  4847  isoeq1  5362  isocnv  5372  isotr  5377  caovordig  5585  caovordg  5587  caovord2d  5589  caovord  5591  ofrfval  5639  ofrval  5641  ofrfval2  5646  caofref  5651  nqtri3or  6249  ltsonq  6251  ltanqg  6253  ltmnqg  6254  lt2addnq  6257  prarloclemarch  6269  ltrnqg  6271  prarloclemlt  6341  addlocprlemgt  6383  mullocprlem  6408  addextpr  6450  recexprlemss1l  6464  recexprlemss1u  6465  recexpr  6467  lttrsr  6508  ltposr  6509  ltsosr  6510  ltasrg  6516  aptisr  6523  mulextsr1lem  6524  mulextsr1  6525  axpre-ltirr  6579  axpre-ltadd  6583  axpre-mulgt0  6584  axpre-mulext  6585  ltadd2  7023  ltadd1  7030  leadd2  7032  reapval  7171  reapmul1  7188  apreim  7195  apirr  7196  apsym  7197  apcotr  7198  remulext  7199  apadd1  7200  apadd2  7201  apneg  7203