Theorem breq12d 3994

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1343   class class class wbr 3981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-br 3982

This theorem is referenced by:  breq123d  3995  3brtr3d  4012  3brtr4d  4013  pocl  4280  csbcnvg  4787  cnvpom  5145  sbcfung  5211  isoeq1  5768  isocnv  5778  isotr  5783  caovordig  6003  caovordg  6005  caovord2d  6007  caovord  6009  ofrfval  6057  ofrval  6059  ofrfval2  6065  caofref  6070  fundmeng  6769  xpsneng  6784  xpcomeng  6790  xpdom2g  6794  phplem3g  6818  php5  6820  php5dom  6825  nqtri3or  7333  ltsonq  7335  ltanqg  7337  ltmnqg  7338  lt2addnq  7341  lt2mulnq  7342  prarloclemarch  7355  ltrnqg  7357  ltnnnq  7360  prarloclemlt  7430  addlocprlemgt  7471  mullocprlem  7507  addextpr  7558  recexprlemss1l  7572  recexprlemss1u  7573  recexpr  7575  caucvgprlemcanl  7581  cauappcvgprlemm  7582  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlemlim  7598  cauappcvgpr  7599  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemcl  7613  caucvgprlemladdrl  7615  caucvgprlem1  7616  caucvgpr  7619  caucvgprprlemell  7622  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemnkeqj  7627  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemloc  7640  caucvgprprlemclphr  7642  caucvgprprlemexb  7644  caucvgprprlem1  7646  lttrsr  7699  ltposr  7700  ltsosr  7701  ltasrg  7707  aptisr  7716  mulextsr1lem  7717  mulextsr1  7718  caucvgsrlemcau  7730  caucvgsrlemgt1  7732  caucvgsrlemoffcau  7735  caucvgsrlemoffres  7737  caucvgsr  7739  axpre-ltirr  7819  axpre-ltadd  7823  axpre-mulgt0  7824  axpre-mulext  7825  axcaucvglemcau  7835  axcaucvglemres  7836  ltadd2  8313  ltadd1  8323  leadd2  8325  reapval  8470  reapmul1  8489  remulext2  8494  apreim  8497  apirr  8499  apsym  8500  apcotr  8501  apadd1  8502  apadd2  8503  apneg  8505  mulext1  8506  mulext2  8507  apti  8516  apsub1  8536  subap0  8537  apmul1  8680  apmul2  8681  apdivmuld  8705  ltmul2  8747  lemul2  8748  ltdiv1  8759  ltdiv2  8778  ledivdiv  8781  lediv2  8782  negiso  8846  div4p1lem1div2  9106  qapne  9573  nn0ledivnn  9699  xleadd1  9807  xltadd1  9808  xltadd2  9809  xsubge0  9813  xleaddadd  9819  qtri3or  10174  frecfzennn  10357  monoord  10407  monoord2  10408  leexp1a  10506  bernneq  10571  apexp1  10627  nn0le2msqd  10628  faclbnd  10650  faclbnd3  10652  faclbnd6  10653  facubnd  10654  fihashdom  10712  zfz1isolemiso  10748  cjap  10844  cvg1nlemcau  10922  cvg1nlemres  10923  resqrexlemlo  10951  resqrexlemcalc3  10954  absext  11001  xrnegiso  11199  xrminltinf  11209  fsumabs  11402  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  fprodle  11577  addmodlteqALT  11793  nn0seqcvgd  11969  algcvg  11976  algcvga  11979  eucalgcvga  11986  qnumgt0  12126  pcprendvds2  12219  pcpremul  12221  ctinfomlemom  12356  ispsmet  12923  psmettri2  12928  ismet  12944  isxmet  12945  xmettri2  12961  blvalps  12988  blval  12989  comet  13099  bdxmet  13101  dvef  13288  cxplt  13436  rpcxple2  13438  rpcxplt2  13439  cxplt3  13440  apcxp2  13458  ltexp2  13460  logbleb  13479  logblt  13480  lgsdilem  13528  apdifflemr  13886  apdiff  13887