Theorem breq12d 4047

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  breq123d  4048  3brtr3d  4065  3brtr4d  4066  pocl  4339  csbcnvg  4851  cnvpom  5213  sbcfung  5283  isoeq1  5851  isocnv  5861  isotr  5866  caovordig  6093  caovordg  6095  caovord2d  6097  caovord  6099  ofrfval  6148  ofrval  6150  ofrfval2  6156  caofref  6164  fundmeng  6875  xpsneng  6890  xpcomeng  6896  xpdom2g  6900  phplem3g  6926  php5  6928  php5dom  6933  exmidpw2en  6982  exmidapne  7343  nqtri3or  7480  ltsonq  7482  ltanqg  7484  ltmnqg  7485  lt2addnq  7488  lt2mulnq  7489  prarloclemarch  7502  ltrnqg  7504  ltnnnq  7507  prarloclemlt  7577  addlocprlemgt  7618  mullocprlem  7654  addextpr  7705  recexprlemss1l  7719  recexprlemss1u  7720  recexpr  7722  caucvgprlemcanl  7728  cauappcvgprlemm  7729  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlemlim  7745  cauappcvgpr  7746  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemcl  7760  caucvgprlemladdrl  7762  caucvgprlem1  7763  caucvgpr  7766  caucvgprprlemell  7769  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemnkeqj  7774  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemloc  7787  caucvgprprlemclphr  7789  caucvgprprlemexb  7791  caucvgprprlem1  7793  lttrsr  7846  ltposr  7847  ltsosr  7848  ltasrg  7854  aptisr  7863  mulextsr1lem  7864  mulextsr1  7865  caucvgsrlemcau  7877  caucvgsrlemgt1  7879  caucvgsrlemoffcau  7882  caucvgsrlemoffres  7884  caucvgsr  7886  axpre-ltirr  7966  axpre-ltadd  7970  axpre-mulgt0  7971  axpre-mulext  7972  axcaucvglemcau  7982  axcaucvglemres  7983  ltadd2  8463  ltadd1  8473  leadd2  8475  reapval  8620  reapmul1  8639  remulext2  8644  apreim  8647  apirr  8649  apsym  8650  apcotr  8651  apadd1  8652  apadd2  8653  apneg  8655  mulext1  8656  mulext2  8657  apti  8666  apsub1  8686  subap0  8687  apmul1  8832  apmul2  8833  apdivmuld  8857  ltmul2  8900  lemul2  8901  ltdiv1  8912  ltdiv2  8931  ledivdiv  8934  lediv2  8935  negiso  8999  div4p1lem1div2  9262  qapne  9730  nn0ledivnn  9859  xleadd1  9967  xltadd1  9968  xltadd2  9969  xsubge0  9973  xleaddadd  9979  qtri3or  10347  frecfzennn  10535  monoord  10594  monoord2  10595  leexp1a  10703  bernneq  10769  apexp1  10827  nn0le2msqd  10828  faclbnd  10850  faclbnd3  10852  faclbnd6  10853  facubnd  10854  fihashdom  10912  zfz1isolemiso  10948  cjap  11088  cvg1nlemcau  11166  cvg1nlemres  11167  resqrexlemlo  11195  resqrexlemcalc3  11198  absext  11245  xrnegiso  11444  xrminltinf  11454  fsumabs  11647  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  fprodle  11822  addmodlteqALT  12041  nn0seqcvgd  12234  algcvg  12241  algcvga  12244  eucalgcvga  12251  qnumgt0  12391  pcprendvds2  12485  pcpremul  12487  pcadd2  12535  2expltfac  12633  ctinfomlemom  12669  gsumfzval  13093  ispsmet  14643  psmettri2  14648  ismet  14664  isxmet  14665  xmettri2  14681  blvalps  14708  blval  14709  comet  14819  bdxmet  14821  dvef  15047  cxplt  15236  rpcxple2  15238  rpcxplt2  15239  cxplt3  15240  apcxp2  15259  ltexp2  15261  logbleb  15281  logblt  15282  lgsdilem  15352  2lgslem1a2  15412  apdifflemr  15778  apdiff  15779