Theorem breq12d 4101

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  breq123d  4102  3brtr3d  4119  3brtr4d  4120  pocl  4400  csbcnvg  4914  cnvpom  5279  sbcfung  5350  isoeq1  5942  isocnv  5952  isotr  5957  caovordig  6188  caovordg  6190  caovord2d  6192  caovord  6194  ofrfval  6244  ofrval  6246  ofrfval2  6252  caofref  6260  fundmeng  6982  xpsneng  7006  xpcomeng  7012  xpdom2g  7016  phplem3g  7042  php5  7044  php5dom  7049  exmidpw2en  7104  exmidapne  7479  nqtri3or  7616  ltsonq  7618  ltanqg  7620  ltmnqg  7621  lt2addnq  7624  lt2mulnq  7625  prarloclemarch  7638  ltrnqg  7640  ltnnnq  7643  prarloclemlt  7713  addlocprlemgt  7754  mullocprlem  7790  addextpr  7841  recexprlemss1l  7855  recexprlemss1u  7856  recexpr  7858  caucvgprlemcanl  7864  cauappcvgprlemm  7865  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  cauappcvgpr  7882  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexb  7927  caucvgprprlem1  7929  lttrsr  7982  ltposr  7983  ltsosr  7984  ltasrg  7990  aptisr  7999  mulextsr1lem  8000  mulextsr1  8001  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  caucvgsr  8022  axpre-ltirr  8102  axpre-ltadd  8106  axpre-mulgt0  8107  axpre-mulext  8108  axcaucvglemcau  8118  axcaucvglemres  8119  ltadd2  8599  ltadd1  8609  leadd2  8611  reapval  8756  reapmul1  8775  remulext2  8780  apreim  8783  apirr  8785  apsym  8786  apcotr  8787  apadd1  8788  apadd2  8789  apneg  8791  mulext1  8792  mulext2  8793  apti  8802  apsub1  8822  subap0  8823  apmul1  8968  apmul2  8969  apdivmuld  8993  ltmul2  9036  lemul2  9037  ltdiv1  9048  ltdiv2  9067  ledivdiv  9070  lediv2  9071  negiso  9135  div4p1lem1div2  9398  qapne  9873  nn0ledivnn  10002  xleadd1  10110  xltadd1  10111  xltadd2  10112  xsubge0  10116  xleaddadd  10122  qtri3or  10500  frecfzennn  10688  monoord  10747  monoord2  10748  leexp1a  10856  bernneq  10922  apexp1  10980  nn0le2msqd  10981  faclbnd  11003  faclbnd3  11005  faclbnd6  11006  facubnd  11007  fihashdom  11066  zfz1isolemiso  11103  cjap  11467  cvg1nlemcau  11545  cvg1nlemres  11546  resqrexlemlo  11574  resqrexlemcalc3  11577  absext  11624  xrnegiso  11823  xrminltinf  11833  fsumabs  12027  cvgratnnlemnexp  12086  cvgratnnlemmn  12087  fprodle  12202  addmodlteqALT  12421  nn0seqcvgd  12614  algcvg  12621  algcvga  12624  eucalgcvga  12631  qnumgt0  12771  pcprendvds2  12865  pcpremul  12867  pcadd2  12915  2expltfac  13013  ctinfomlemom  13049  gsumfzval  13475  mplsubgfilemcl  14715  ispsmet  15049  psmettri2  15054  ismet  15070  isxmet  15071  xmettri2  15087  blvalps  15114  blval  15115  comet  15225  bdxmet  15227  dvef  15453  cxplt  15642  rpcxple2  15644  rpcxplt2  15645  cxplt3  15646  apcxp2  15665  ltexp2  15667  logbleb  15687  logblt  15688  lgsdilem  15758  2lgslem1a2  15818  apdifflemr  16654  apdiff  16655