Theorem breq12d 4143

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  breq123d  4144  3brtr3d  4161  3brtr4d  4162  pocl  4448  csbcnvg  4964  cnvpom  5330  sbcfung  5401  isoeq1  6007  isocnv  6017  isotr  6022  caovordig  6255  caovordg  6257  caovord2d  6259  caovord  6261  ofrfval  6311  ofrval  6313  ofrfval2  6319  caofref  6327  fundmeng  7095  xpsneng  7120  xpcomeng  7126  xpdom2g  7130  phplem3g  7157  php5  7159  php5dom  7164  exmidpw2en  7219  papirr  7612  exmidapne  7627  nqtri3or  7764  ltsonq  7766  ltanqg  7768  ltmnqg  7769  lt2addnq  7772  lt2mulnq  7773  prarloclemarch  7786  ltrnqg  7788  ltnnnq  7791  prarloclemlt  7861  addlocprlemgt  7902  mullocprlem  7938  addextpr  7989  recexprlemss1l  8003  recexprlemss1u  8004  recexpr  8006  caucvgprlemcanl  8012  cauappcvgprlemm  8013  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlemlim  8029  cauappcvgpr  8030  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgpr  8050  caucvgprprlemell  8053  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnkeqj  8058  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemloc  8071  caucvgprprlemclphr  8073  caucvgprprlemexb  8075  caucvgprprlem1  8077  lttrsr  8130  ltposr  8131  ltsosr  8132  ltasrg  8138  aptisr  8147  mulextsr1lem  8148  mulextsr1  8149  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  caucvgsr  8170  axpre-ltirr  8250  axpre-ltadd  8254  axpre-mulgt0  8255  axpre-mulext  8256  axcaucvglemcau  8266  axcaucvglemres  8267  ltadd2  8749  ltadd1  8759  leadd2  8761  reapval  8907  reapmul1  8926  remulext2  8931  apreim  8934  apirr  8936  apsym  8937  apcotr  8938  apadd1  8939  apadd2  8940  apneg  8942  mulext1  8943  mulext2  8944  apti  8953  apsub1  8973  subap0  8974  apmul1  9121  apmul2  9122  apdivmuld  9146  ltmul2  9189  lemul2  9190  ltdiv1  9201  ltdiv2  9220  ledivdiv  9223  lediv2  9224  negiso  9288  div4p1lem1div2  9564  qapne  10049  nn0ledivnn  10179  xleadd1  10288  xltadd1  10289  xltadd2  10290  xsubge0  10294  xleaddadd  10300  qtri3or  10686  frecfzennn  10878  monoord  10937  monoord2  10938  leexp1a  11046  bernneq  11113  apexp1  11172  nn0le2msqd  11173  faclbnd  11195  faclbnd3  11197  faclbnd6  11198  facubnd  11199  fihashdom  11259  zfz1isolemiso  11307  cjap  11688  cvg1nlemcau  11766  cvg1nlemres  11767  resqrexlemlo  11795  resqrexlemcalc3  11798  absext  11845  xrnegiso  12047  xrminltinf  12057  fsumabs  12251  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  fprodle  12426  addmodlteqALT  12645  nn0seqcvgd  12838  algcvg  12845  algcvga  12848  eucalgcvga  12855  qnumgt0  12997  pcprendvds2  13093  pcpremul  13095  pcadd2  13143  2expltfac  13242  ctinfomlemom  13370  gzsumfzval  13764  mplsubgfilemcl  15189  ispsmet  15523  psmettri2  15528  ismet  15544  isxmet  15545  xmettri2  15561  blvalps  15588  blval  15589  comet  15699  bdxmet  15701  dvef  15927  cxplt  16125  rpcxple2  16127  rpcxplt2  16128  cxplt3  16129  apcxp2  16148  ltexp2  16151  logbleb  16171  logblt  16172  pellexlem3  16205  ppiqltx  16255  chtqub  16270  bclbnd  16281  prmefexple  16282  bposlem5  16289  bposlem6  16290  bposlem7  16291  lgsdilem  16325  2lgslem1a2  16385  apdifflemr  17276  apdiff  17277