Theorem breq12d 4095

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   class class class wbr 4082

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083

This theorem is referenced by:  breq123d  4096  3brtr3d  4113  3brtr4d  4114  pocl  4393  csbcnvg  4905  cnvpom  5270  sbcfung  5341  isoeq1  5924  isocnv  5934  isotr  5939  caovordig  6170  caovordg  6172  caovord2d  6174  caovord  6176  ofrfval  6225  ofrval  6227  ofrfval2  6233  caofref  6241  fundmeng  6958  xpsneng  6977  xpcomeng  6983  xpdom2g  6987  phplem3g  7013  php5  7015  php5dom  7020  exmidpw2en  7070  exmidapne  7442  nqtri3or  7579  ltsonq  7581  ltanqg  7583  ltmnqg  7584  lt2addnq  7587  lt2mulnq  7588  prarloclemarch  7601  ltrnqg  7603  ltnnnq  7606  prarloclemlt  7676  addlocprlemgt  7717  mullocprlem  7753  addextpr  7804  recexprlemss1l  7818  recexprlemss1u  7819  recexpr  7821  caucvgprlemcanl  7827  cauappcvgprlemm  7828  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem1  7842  cauappcvgprlemlim  7844  cauappcvgpr  7845  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlemcl  7859  caucvgprlemladdrl  7861  caucvgprlem1  7862  caucvgpr  7865  caucvgprprlemell  7868  caucvgprprlemcbv  7870  caucvgprprlemval  7871  caucvgprprlemnkeqj  7873  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemloc  7886  caucvgprprlemclphr  7888  caucvgprprlemexb  7890  caucvgprprlem1  7892  lttrsr  7945  ltposr  7946  ltsosr  7947  ltasrg  7953  aptisr  7962  mulextsr1lem  7963  mulextsr1  7964  caucvgsrlemcau  7976  caucvgsrlemgt1  7978  caucvgsrlemoffcau  7981  caucvgsrlemoffres  7983  caucvgsr  7985  axpre-ltirr  8065  axpre-ltadd  8069  axpre-mulgt0  8070  axpre-mulext  8071  axcaucvglemcau  8081  axcaucvglemres  8082  ltadd2  8562  ltadd1  8572  leadd2  8574  reapval  8719  reapmul1  8738  remulext2  8743  apreim  8746  apirr  8748  apsym  8749  apcotr  8750  apadd1  8751  apadd2  8752  apneg  8754  mulext1  8755  mulext2  8756  apti  8765  apsub1  8785  subap0  8786  apmul1  8931  apmul2  8932  apdivmuld  8956  ltmul2  8999  lemul2  9000  ltdiv1  9011  ltdiv2  9030  ledivdiv  9033  lediv2  9034  negiso  9098  div4p1lem1div2  9361  qapne  9830  nn0ledivnn  9959  xleadd1  10067  xltadd1  10068  xltadd2  10069  xsubge0  10073  xleaddadd  10079  qtri3or  10455  frecfzennn  10643  monoord  10702  monoord2  10703  leexp1a  10811  bernneq  10877  apexp1  10935  nn0le2msqd  10936  faclbnd  10958  faclbnd3  10960  faclbnd6  10961  facubnd  10962  fihashdom  11020  zfz1isolemiso  11056  cjap  11412  cvg1nlemcau  11490  cvg1nlemres  11491  resqrexlemlo  11519  resqrexlemcalc3  11522  absext  11569  xrnegiso  11768  xrminltinf  11778  fsumabs  11971  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  fprodle  12146  addmodlteqALT  12365  nn0seqcvgd  12558  algcvg  12565  algcvga  12568  eucalgcvga  12575  qnumgt0  12715  pcprendvds2  12809  pcpremul  12811  pcadd2  12859  2expltfac  12957  ctinfomlemom  12993  gsumfzval  13419  mplsubgfilemcl  14657  ispsmet  14991  psmettri2  14996  ismet  15012  isxmet  15013  xmettri2  15029  blvalps  15056  blval  15057  comet  15167  bdxmet  15169  dvef  15395  cxplt  15584  rpcxple2  15586  rpcxplt2  15587  cxplt3  15588  apcxp2  15607  ltexp2  15609  logbleb  15629  logblt  15630  lgsdilem  15700  2lgslem1a2  15760  apdifflemr  16374  apdiff  16375