Theorem breqan12d 5113

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypotheses

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
breqan12i.2	⊢ (𝜓 → 𝐶 = 𝐷)

Assertion

Ref	Expression
breqan12d	⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Proof of Theorem breqan12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breqan12i.2	. 2 ⊢ (𝜓 → 𝐶 = 𝐷)
3		breq12 5102	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2an 597	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   class class class wbr 5097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  breqan12rd  5114  soisores  7273  isoid  7275  isores3  7281  isoini2  7285  ofrfvalg  7630  fnwelem  8073  fnse  8075  infsupprpr  9411  wemaplem1  9453  r0weon  9924  sornom  10189  enqbreq2  10833  nqereu  10842  ordpinq  10856  lterpq  10883  ltresr2  11054  axpre-ltadd  11080  leltadd  11623  lemul1a  11997  negiso  12124  xltneg  13134  lt2sq  14058  le2sq  14059  expmordi  14092  sqrtle  15185  prdsleval  17399  efgcpbllema  19685  iducn  24228  icopnfhmeo  24899  iccpnfhmeo  24901  xrhmeo  24902  reefiso  26416  sinord  26501  logltb  26567  logccv  26630  atanord  26895  birthdaylem3  26921  lgsquadlem3  27351  sltneg  28025  onsiso  28250  mddmd  32357  xrge0iifiso  34071  revwlkb  35299  erdszelem4  35367  erdszelem8  35371  satfv0  35531  cgrextend  36181  matunitlindf  37788  idlaut  40391  monotuz  43220  monotoddzzfi  43221  wepwsolem  43321  fnwe2val  43328  aomclem8  43340  isgrlim  48265  rrx2plord  49003  rrx2plordisom  49006