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  11188  cvg1nlemcau  11266  cvg1nlemres  11267  resqrexlemlo  11295  resqrexlemcalc3  11298  absext  11345  xrnegiso  11544  xrminltinf  11554  fsumabs  11747  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  fprodle  11922  addmodlteqALT  12141  nn0seqcvgd  12334  algcvg  12341  algcvga  12344  eucalgcvga  12351  qnumgt0  12491  pcprendvds2  12585  pcpremul  12587  pcadd2  12635  2expltfac  12733  ctinfomlemom  12769  gsumfzval  13194  mplsubgfilemcl  14432  ispsmet  14766  psmettri2  14771  ismet  14787  isxmet  14788  xmettri2  14804  blvalps  14831  blval  14832  comet  14942  bdxmet  14944  dvef  15170  cxplt  15359  rpcxple2  15361  rpcxplt2  15362  cxplt3  15363  apcxp2  15382  ltexp2  15384  logbleb  15404  logblt  15405  lgsdilem  15475  2lgslem1a2  15535  apdifflemr  15948  apdiff  15949