Theorem breq12d 4042

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   class class class wbr 4029

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030

This theorem is referenced by:  breq123d  4043  3brtr3d  4060  3brtr4d  4061  pocl  4334  csbcnvg  4846  cnvpom  5208  sbcfung  5278  isoeq1  5844  isocnv  5854  isotr  5859  caovordig  6084  caovordg  6086  caovord2d  6088  caovord  6090  ofrfval  6139  ofrval  6141  ofrfval2  6147  caofref  6154  fundmeng  6861  xpsneng  6876  xpcomeng  6882  xpdom2g  6886  phplem3g  6912  php5  6914  php5dom  6919  exmidpw2en  6968  exmidapne  7320  nqtri3or  7456  ltsonq  7458  ltanqg  7460  ltmnqg  7461  lt2addnq  7464  lt2mulnq  7465  prarloclemarch  7478  ltrnqg  7480  ltnnnq  7483  prarloclemlt  7553  addlocprlemgt  7594  mullocprlem  7630  addextpr  7681  recexprlemss1l  7695  recexprlemss1u  7696  recexpr  7698  caucvgprlemcanl  7704  cauappcvgprlemm  7705  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlemlim  7721  cauappcvgpr  7722  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemcl  7736  caucvgprlemladdrl  7738  caucvgprlem1  7739  caucvgpr  7742  caucvgprprlemell  7745  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemnkeqj  7750  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemloc  7763  caucvgprprlemclphr  7765  caucvgprprlemexb  7767  caucvgprprlem1  7769  lttrsr  7822  ltposr  7823  ltsosr  7824  ltasrg  7830  aptisr  7839  mulextsr1lem  7840  mulextsr1  7841  caucvgsrlemcau  7853  caucvgsrlemgt1  7855  caucvgsrlemoffcau  7858  caucvgsrlemoffres  7860  caucvgsr  7862  axpre-ltirr  7942  axpre-ltadd  7946  axpre-mulgt0  7947  axpre-mulext  7948  axcaucvglemcau  7958  axcaucvglemres  7959  ltadd2  8438  ltadd1  8448  leadd2  8450  reapval  8595  reapmul1  8614  remulext2  8619  apreim  8622  apirr  8624  apsym  8625  apcotr  8626  apadd1  8627  apadd2  8628  apneg  8630  mulext1  8631  mulext2  8632  apti  8641  apsub1  8661  subap0  8662  apmul1  8807  apmul2  8808  apdivmuld  8832  ltmul2  8875  lemul2  8876  ltdiv1  8887  ltdiv2  8906  ledivdiv  8909  lediv2  8910  negiso  8974  div4p1lem1div2  9236  qapne  9704  nn0ledivnn  9833  xleadd1  9941  xltadd1  9942  xltadd2  9943  xsubge0  9947  xleaddadd  9953  qtri3or  10310  frecfzennn  10497  monoord  10556  monoord2  10557  leexp1a  10665  bernneq  10731  apexp1  10789  nn0le2msqd  10790  faclbnd  10812  faclbnd3  10814  faclbnd6  10815  facubnd  10816  fihashdom  10874  zfz1isolemiso  10910  cjap  11050  cvg1nlemcau  11128  cvg1nlemres  11129  resqrexlemlo  11157  resqrexlemcalc3  11160  absext  11207  xrnegiso  11405  xrminltinf  11415  fsumabs  11608  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  fprodle  11783  addmodlteqALT  12001  nn0seqcvgd  12179  algcvg  12186  algcvga  12189  eucalgcvga  12196  qnumgt0  12336  pcprendvds2  12429  pcpremul  12431  pcadd2  12479  ctinfomlemom  12584  gsumfzval  12974  ispsmet  14491  psmettri2  14496  ismet  14512  isxmet  14513  xmettri2  14529  blvalps  14556  blval  14557  comet  14667  bdxmet  14669  dvef  14873  cxplt  15050  rpcxple2  15052  rpcxplt2  15053  cxplt3  15054  apcxp2  15072  ltexp2  15074  logbleb  15093  logblt  15094  lgsdilem  15143  apdifflemr  15537  apdiff  15538