Theorem breqan12d 5091

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 5080	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2an 603	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  breqan12rd  5092  soisores  7275  isoid  7277  isores3  7283  isoini2  7287  ofrfvalg  7632  fnwelem  8075  fnse  8077  infsupprpr  9413  wemaplem1  9455  r0weon  9929  sornom  10194  enqbreq2  10838  nqereu  10847  ordpinq  10861  lterpq  10888  ltresr2  11059  axpre-ltadd  11085  leltadd  11629  lemul1a  12004  negiso  12131  xltneg  13164  lt2sq  14090  le2sq  14091  expmordi  14124  sqrtle  15217  prdsleval  17435  efgcpbllema  19724  iducn  24269  icopnfhmeo  24932  iccpnfhmeo  24934  xrhmeo  24935  reefiso  26435  sinord  26520  logltb  26586  logccv  26649  atanord  26913  birthdaylem3  26939  lgsquadlem3  27367  ltnegs  28059  oniso  28285  mddmd  32394  xrge0iifiso  34131  revwlkb  35369  erdszelem4  35437  erdszelem8  35441  satfv0  35601  cgrextend  36251  matunitlindf  38000  idlaut  40603  monotuz  43401  monotoddzzfi  43402  wepwsolem  43502  fnwe2val  43509  aomclem8  43521  isgrlim  48487  rrx2plord  49225  rrx2plordisom  49228