Theorem breq12d 3950

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332   class class class wbr 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-br 3938

This theorem is referenced by:  breq123d  3951  3brtr3d  3967  3brtr4d  3968  pocl  4233  csbcnvg  4731  cnvpom  5089  sbcfung  5155  isoeq1  5710  isocnv  5720  isotr  5725  caovordig  5944  caovordg  5946  caovord2d  5948  caovord  5950  ofrfval  5998  ofrval  6000  ofrfval2  6006  caofref  6011  fundmeng  6709  xpsneng  6724  xpcomeng  6730  xpdom2g  6734  phplem3g  6758  php5  6760  php5dom  6765  nqtri3or  7228  ltsonq  7230  ltanqg  7232  ltmnqg  7233  lt2addnq  7236  lt2mulnq  7237  prarloclemarch  7250  ltrnqg  7252  ltnnnq  7255  prarloclemlt  7325  addlocprlemgt  7366  mullocprlem  7402  addextpr  7453  recexprlemss1l  7467  recexprlemss1u  7468  recexpr  7470  caucvgprlemcanl  7476  cauappcvgprlemm  7477  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  cauappcvgprlemlim  7493  cauappcvgpr  7494  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemcl  7508  caucvgprlemladdrl  7510  caucvgprlem1  7511  caucvgpr  7514  caucvgprprlemell  7517  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemnkeqj  7522  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemloc  7535  caucvgprprlemclphr  7537  caucvgprprlemexb  7539  caucvgprprlem1  7541  lttrsr  7594  ltposr  7595  ltsosr  7596  ltasrg  7602  aptisr  7611  mulextsr1lem  7612  mulextsr1  7613  caucvgsrlemcau  7625  caucvgsrlemgt1  7627  caucvgsrlemoffcau  7630  caucvgsrlemoffres  7632  caucvgsr  7634  axpre-ltirr  7714  axpre-ltadd  7718  axpre-mulgt0  7719  axpre-mulext  7720  axcaucvglemcau  7730  axcaucvglemres  7731  ltadd2  8205  ltadd1  8215  leadd2  8217  reapval  8362  reapmul1  8381  remulext2  8386  apreim  8389  apirr  8391  apsym  8392  apcotr  8393  apadd1  8394  apadd2  8395  apneg  8397  mulext1  8398  mulext2  8399  apti  8408  apsub1  8428  subap0  8429  apmul1  8572  apmul2  8573  apdivmuld  8597  ltmul2  8638  lemul2  8639  ltdiv1  8650  ltdiv2  8669  ledivdiv  8672  lediv2  8673  negiso  8737  div4p1lem1div2  8997  qapne  9458  nn0ledivnn  9584  xleadd1  9688  xltadd1  9689  xltadd2  9690  xsubge0  9694  xleaddadd  9700  qtri3or  10051  frecfzennn  10230  monoord  10280  monoord2  10281  leexp1a  10379  bernneq  10443  apexp1  10496  nn0le2msqd  10497  faclbnd  10519  faclbnd3  10521  faclbnd6  10522  facubnd  10523  fihashdom  10581  zfz1isolemiso  10614  cjap  10710  cvg1nlemcau  10788  cvg1nlemres  10789  resqrexlemlo  10817  resqrexlemcalc3  10820  absext  10867  xrnegiso  11063  xrminltinf  11073  fsumabs  11266  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  addmodlteqALT  11593  nn0seqcvgd  11758  algcvg  11765  algcvga  11768  eucalgcvga  11775  qnumgt0  11912  ctinfomlemom  11976  ispsmet  12531  psmettri2  12536  ismet  12552  isxmet  12553  xmettri2  12569  blvalps  12596  blval  12597  comet  12707  bdxmet  12709  dvef  12896  cxplt  13044  rpcxple2  13046  rpcxplt2  13047  cxplt3  13048  apcxp2  13066  logbleb  13086  logblt  13087  apdifflemr  13415  apdiff  13416