Theorem breq12d 3767

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 3759	. 2 ⊢ ((A = B ∧ 𝐶 = 𝐷) → (A𝑅𝐶 ↔ B𝑅𝐷))
4	1, 2, 3	syl2anc 391	1 ⊢ (φ → (A𝑅𝐶 ↔ B𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1242   class class class wbr 3754

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-sn 3372  df-pr 3373  df-op 3375  df-br 3755

This theorem is referenced by:  breq123d  3768  3brtr3d  3783  3brtr4d  3784  pocl  4030  csbcnvg  4461  cnvpom  4802  sbcfung  4866  isoeq1  5382  isocnv  5392  isotr  5397  caovordig  5605  caovordg  5607  caovord2d  5609  caovord  5611  ofrfval  5659  ofrval  5661  ofrfval2  5666  caofref  5671  fundmeng  6216  xpsneng  6225  xpcomeng  6231  xpdom2g  6235  nqtri3or  6373  ltsonq  6375  ltanqg  6377  ltmnqg  6378  lt2addnq  6381  prarloclemarch  6394  ltrnqg  6396  prarloclemlt  6468  addlocprlemgt  6510  mullocprlem  6541  addextpr  6583  recexprlemss1l  6597  recexprlemss1u  6598  recexpr  6600  lttrsr  6642  ltposr  6643  ltsosr  6644  ltasrg  6650  aptisr  6657  mulextsr1lem  6658  mulextsr1  6659  axpre-ltirr  6718  axpre-ltadd  6722  axpre-mulgt0  6723  axpre-mulext  6724  ltadd2  7164  ltadd1  7171  leadd2  7173  reapval  7312  reapmul1  7331  remulext2  7336  apreim  7339  apirr  7341  apsym  7342  apcotr  7343  apadd1  7344  apadd2  7345  apneg  7347  mulext1  7348  mulext2  7349  apti  7358  apmul1  7498  ltmul2  7554  lemul2  7555  ltdiv1  7566  ltdiv2  7585  ledivdiv  7588  lediv2  7589  qapne  8299  frecfzennn  8822