Theorem breq12d 3777

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

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1243   class class class wbr 3764

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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-br 3765

This theorem is referenced by:  breq123d  3778  3brtr3d  3793  3brtr4d  3794  pocl  4040  csbcnvg  4519  cnvpom  4860  sbcfung  4925  isoeq1  5441  isocnv  5451  isotr  5456  caovordig  5666  caovordg  5668  caovord2d  5670  caovord  5672  ofrfval  5720  ofrval  5722  ofrfval2  5727  caofref  5732  fundmeng  6287  xpsneng  6296  xpcomeng  6302  xpdom2g  6306  phplem3g  6319  php5  6321  php5dom  6325  nqtri3or  6494  ltsonq  6496  ltanqg  6498  ltmnqg  6499  lt2addnq  6502  lt2mulnq  6503  prarloclemarch  6516  ltrnqg  6518  ltnnnq  6521  prarloclemlt  6591  addlocprlemgt  6632  mullocprlem  6668  addextpr  6719  recexprlemss1l  6733  recexprlemss1u  6734  recexpr  6736  caucvgprlemcanl  6742  cauappcvgprlemm  6743  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  cauappcvgprlemlim  6759  cauappcvgpr  6760  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemcl  6774  caucvgprlemladdrl  6776  caucvgprlem1  6777  caucvgpr  6780  caucvgprprlemell  6783  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemnkeqj  6788  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemloc  6801  caucvgprprlemclphr  6803  caucvgprprlemexb  6805  caucvgprprlem1  6807  lttrsr  6847  ltposr  6848  ltsosr  6849  ltasrg  6855  aptisr  6863  mulextsr1lem  6864  mulextsr1  6865  caucvgsrlemcau  6877  caucvgsrlemgt1  6879  caucvgsrlemoffcau  6882  caucvgsrlemoffres  6884  caucvgsr  6886  axpre-ltirr  6956  axpre-ltadd  6960  axpre-mulgt0  6961  axpre-mulext  6962  axcaucvglemcau  6972  axcaucvglemres  6973  ltadd2  7416  ltadd1  7424  leadd2  7426  reapval  7567  reapmul1  7586  remulext2  7591  apreim  7594  apirr  7596  apsym  7597  apcotr  7598  apadd1  7599  apadd2  7600  apneg  7602  mulext1  7603  mulext2  7604  apti  7613  apmul1  7764  ltmul2  7822  lemul2  7823  ltdiv1  7834  ltdiv2  7853  ledivdiv  7856  lediv2  7857  div4p1lem1div2  8177  qapne  8574  qtri3or  9098  frecfzennn  9203  monoord  9235  monoord2  9236  leexp1a  9309  bernneq  9369  cjap  9506  cvg1nlemcau  9583  cvg1nlemres  9584  resqrexlemlo  9611  resqrexlemcalc3  9614  absext  9661  nn0seqcvgd  9880  ialgcvg  9887  ialgcvga  9890