Theorem breq12d 4127

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  breq123d  4128  3brtr3d  4145  3brtr4d  4146  pocl  4429  csbcnvg  4944  cnvpom  5310  sbcfung  5381  isoeq1  5980  isocnv  5990  isotr  5995  caovordig  6228  caovordg  6230  caovord2d  6232  caovord  6234  ofrfval  6284  ofrval  6286  ofrfval2  6292  caofref  6300  fundmeng  7061  xpsneng  7086  xpcomeng  7092  xpdom2g  7096  phplem3g  7123  php5  7125  php5dom  7130  exmidpw2en  7185  papirr  7575  exmidapne  7590  nqtri3or  7727  ltsonq  7729  ltanqg  7731  ltmnqg  7732  lt2addnq  7735  lt2mulnq  7736  prarloclemarch  7749  ltrnqg  7751  ltnnnq  7754  prarloclemlt  7824  addlocprlemgt  7865  mullocprlem  7901  addextpr  7952  recexprlemss1l  7966  recexprlemss1u  7967  recexpr  7969  caucvgprlemcanl  7975  cauappcvgprlemm  7976  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlemlim  7992  cauappcvgpr  7993  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgpr  8013  caucvgprprlemell  8016  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnkeqj  8021  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexb  8038  caucvgprprlem1  8040  lttrsr  8093  ltposr  8094  ltsosr  8095  ltasrg  8101  aptisr  8110  mulextsr1lem  8111  mulextsr1  8112  caucvgsrlemcau  8124  caucvgsrlemgt1  8126  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  caucvgsr  8133  axpre-ltirr  8213  axpre-ltadd  8217  axpre-mulgt0  8218  axpre-mulext  8219  axcaucvglemcau  8229  axcaucvglemres  8230  ltadd2  8710  ltadd1  8720  leadd2  8722  reapval  8867  reapmul1  8886  remulext2  8891  apreim  8894  apirr  8896  apsym  8897  apcotr  8898  apadd1  8899  apadd2  8900  apneg  8902  mulext1  8903  mulext2  8904  apti  8913  apsub1  8933  subap0  8934  apmul1  9079  apmul2  9080  apdivmuld  9104  ltmul2  9147  lemul2  9148  ltdiv1  9159  ltdiv2  9178  ledivdiv  9181  lediv2  9182  negiso  9246  div4p1lem1div2  9509  qapne  9989  nn0ledivnn  10118  xleadd1  10227  xltadd1  10228  xltadd2  10229  xsubge0  10233  xleaddadd  10239  qtri3or  10624  frecfzennn  10812  monoord  10871  monoord2  10872  leexp1a  10980  bernneq  11047  apexp1  11105  nn0le2msqd  11106  faclbnd  11128  faclbnd3  11130  faclbnd6  11131  facubnd  11132  fihashdom  11192  zfz1isolemiso  11236  cjap  11616  cvg1nlemcau  11694  cvg1nlemres  11695  resqrexlemlo  11723  resqrexlemcalc3  11726  absext  11773  xrnegiso  11972  xrminltinf  11982  fsumabs  12176  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  fprodle  12351  addmodlteqALT  12570  nn0seqcvgd  12763  algcvg  12770  algcvga  12773  eucalgcvga  12780  qnumgt0  12920  pcprendvds2  13014  pcpremul  13016  pcadd2  13064  2expltfac  13162  ctinfomlemom  13262  gsumfzval  13654  mplsubgfilemcl  14980  ispsmet  15314  psmettri2  15319  ismet  15335  isxmet  15336  xmettri2  15352  blvalps  15379  blval  15380  comet  15490  bdxmet  15492  dvef  15718  cxplt  15907  rpcxple2  15909  rpcxplt2  15910  cxplt3  15911  apcxp2  15930  ltexp2  15932  logbleb  15952  logblt  15953  pellexlem3  15973  lgsdilem  16026  2lgslem1a2  16086  apdifflemr  16957  apdiff  16958