Theorem breq12d 4056

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1372   class class class wbr 4043

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044

This theorem is referenced by:  breq123d  4057  3brtr3d  4074  3brtr4d  4075  pocl  4349  csbcnvg  4861  cnvpom  5224  sbcfung  5294  isoeq1  5869  isocnv  5879  isotr  5884  caovordig  6111  caovordg  6113  caovord2d  6115  caovord  6117  ofrfval  6166  ofrval  6168  ofrfval2  6174  caofref  6182  fundmeng  6898  xpsneng  6916  xpcomeng  6922  xpdom2g  6926  phplem3g  6952  php5  6954  php5dom  6959  exmidpw2en  7008  exmidapne  7371  nqtri3or  7508  ltsonq  7510  ltanqg  7512  ltmnqg  7513  lt2addnq  7516  lt2mulnq  7517  prarloclemarch  7530  ltrnqg  7532  ltnnnq  7535  prarloclemlt  7605  addlocprlemgt  7646  mullocprlem  7682  addextpr  7733  recexprlemss1l  7747  recexprlemss1u  7748  recexpr  7750  caucvgprlemcanl  7756  cauappcvgprlemm  7757  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem1  7771  cauappcvgprlemlim  7773  cauappcvgpr  7774  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemcl  7788  caucvgprlemladdrl  7790  caucvgprlem1  7791  caucvgpr  7794  caucvgprprlemell  7797  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemnkeqj  7802  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemloc  7815  caucvgprprlemclphr  7817  caucvgprprlemexb  7819  caucvgprprlem1  7821  lttrsr  7874  ltposr  7875  ltsosr  7876  ltasrg  7882  aptisr  7891  mulextsr1lem  7892  mulextsr1  7893  caucvgsrlemcau  7905  caucvgsrlemgt1  7907  caucvgsrlemoffcau  7910  caucvgsrlemoffres  7912  caucvgsr  7914  axpre-ltirr  7994  axpre-ltadd  7998  axpre-mulgt0  7999  axpre-mulext  8000  axcaucvglemcau  8010  axcaucvglemres  8011  ltadd2  8491  ltadd1  8501  leadd2  8503  reapval  8648  reapmul1  8667  remulext2  8672  apreim  8675  apirr  8677  apsym  8678  apcotr  8679  apadd1  8680  apadd2  8681  apneg  8683  mulext1  8684  mulext2  8685  apti  8694  apsub1  8714  subap0  8715  apmul1  8860  apmul2  8861  apdivmuld  8885  ltmul2  8928  lemul2  8929  ltdiv1  8940  ltdiv2  8959  ledivdiv  8962  lediv2  8963  negiso  9027  div4p1lem1div2  9290  qapne  9759  nn0ledivnn  9888  xleadd1  9996  xltadd1  9997  xltadd2  9998  xsubge0  10002  xleaddadd  10008  qtri3or  10381  frecfzennn  10569  monoord  10628  monoord2  10629  leexp1a  10737  bernneq  10803  apexp1  10861  nn0le2msqd  10862  faclbnd  10884  faclbnd3  10886  faclbnd6  10887  facubnd  10888  fihashdom  10946  zfz1isolemiso  10982  cjap  11159  cvg1nlemcau  11237  cvg1nlemres  11238  resqrexlemlo  11266  resqrexlemcalc3  11269  absext  11316  xrnegiso  11515  xrminltinf  11525  fsumabs  11718  cvgratnnlemnexp  11777  cvgratnnlemmn  11778  fprodle  11893  addmodlteqALT  12112  nn0seqcvgd  12305  algcvg  12312  algcvga  12315  eucalgcvga  12322  qnumgt0  12462  pcprendvds2  12556  pcpremul  12558  pcadd2  12606  2expltfac  12704  ctinfomlemom  12740  gsumfzval  13165  mplsubgfilemcl  14403  ispsmet  14737  psmettri2  14742  ismet  14758  isxmet  14759  xmettri2  14775  blvalps  14802  blval  14803  comet  14913  bdxmet  14915  dvef  15141  cxplt  15330  rpcxple2  15332  rpcxplt2  15333  cxplt3  15334  apcxp2  15353  ltexp2  15355  logbleb  15375  logblt  15376  lgsdilem  15446  2lgslem1a2  15506  apdifflemr  15919  apdiff  15920