Theorem breq12d 4099

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

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

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087

This theorem is referenced by:  breq123d  4100  3brtr3d  4117  3brtr4d  4118  pocl  4398  csbcnvg  4912  cnvpom  5277  sbcfung  5348  isoeq1  5937  isocnv  5947  isotr  5952  caovordig  6183  caovordg  6185  caovord2d  6187  caovord  6189  ofrfval  6239  ofrval  6241  ofrfval2  6247  caofref  6255  fundmeng  6977  xpsneng  7001  xpcomeng  7007  xpdom2g  7011  phplem3g  7037  php5  7039  php5dom  7044  exmidpw2en  7097  exmidapne  7469  nqtri3or  7606  ltsonq  7608  ltanqg  7610  ltmnqg  7611  lt2addnq  7614  lt2mulnq  7615  prarloclemarch  7628  ltrnqg  7630  ltnnnq  7633  prarloclemlt  7703  addlocprlemgt  7744  mullocprlem  7780  addextpr  7831  recexprlemss1l  7845  recexprlemss1u  7846  recexpr  7848  caucvgprlemcanl  7854  cauappcvgprlemm  7855  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlemlim  7871  cauappcvgpr  7872  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemcl  7886  caucvgprlemladdrl  7888  caucvgprlem1  7889  caucvgpr  7892  caucvgprprlemell  7895  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemnkeqj  7900  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemloc  7913  caucvgprprlemclphr  7915  caucvgprprlemexb  7917  caucvgprprlem1  7919  lttrsr  7972  ltposr  7973  ltsosr  7974  ltasrg  7980  aptisr  7989  mulextsr1lem  7990  mulextsr1  7991  caucvgsrlemcau  8003  caucvgsrlemgt1  8005  caucvgsrlemoffcau  8008  caucvgsrlemoffres  8010  caucvgsr  8012  axpre-ltirr  8092  axpre-ltadd  8096  axpre-mulgt0  8097  axpre-mulext  8098  axcaucvglemcau  8108  axcaucvglemres  8109  ltadd2  8589  ltadd1  8599  leadd2  8601  reapval  8746  reapmul1  8765  remulext2  8770  apreim  8773  apirr  8775  apsym  8776  apcotr  8777  apadd1  8778  apadd2  8779  apneg  8781  mulext1  8782  mulext2  8783  apti  8792  apsub1  8812  subap0  8813  apmul1  8958  apmul2  8959  apdivmuld  8983  ltmul2  9026  lemul2  9027  ltdiv1  9038  ltdiv2  9057  ledivdiv  9060  lediv2  9061  negiso  9125  div4p1lem1div2  9388  qapne  9863  nn0ledivnn  9992  xleadd1  10100  xltadd1  10101  xltadd2  10102  xsubge0  10106  xleaddadd  10112  qtri3or  10490  frecfzennn  10678  monoord  10737  monoord2  10738  leexp1a  10846  bernneq  10912  apexp1  10970  nn0le2msqd  10971  faclbnd  10993  faclbnd3  10995  faclbnd6  10996  facubnd  10997  fihashdom  11056  zfz1isolemiso  11093  cjap  11457  cvg1nlemcau  11535  cvg1nlemres  11536  resqrexlemlo  11564  resqrexlemcalc3  11567  absext  11614  xrnegiso  11813  xrminltinf  11823  fsumabs  12016  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  fprodle  12191  addmodlteqALT  12410  nn0seqcvgd  12603  algcvg  12610  algcvga  12613  eucalgcvga  12620  qnumgt0  12760  pcprendvds2  12854  pcpremul  12856  pcadd2  12904  2expltfac  13002  ctinfomlemom  13038  gsumfzval  13464  mplsubgfilemcl  14703  ispsmet  15037  psmettri2  15042  ismet  15058  isxmet  15059  xmettri2  15075  blvalps  15102  blval  15103  comet  15213  bdxmet  15215  dvef  15441  cxplt  15630  rpcxple2  15632  rpcxplt2  15633  cxplt3  15634  apcxp2  15653  ltexp2  15655  logbleb  15675  logblt  15676  lgsdilem  15746  2lgslem1a2  15806  apdifflemr  16587  apdiff  16588