Theorem breqan12d 5116

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  breqan12rd  5117  soisores  7285  isoid  7287  isores3  7293  isoini2  7297  ofrfvalg  7642  fnwelem  8085  fnse  8087  infsupprpr  9423  wemaplem1  9465  r0weon  9936  sornom  10201  enqbreq2  10845  nqereu  10854  ordpinq  10868  lterpq  10895  ltresr2  11066  axpre-ltadd  11092  leltadd  11635  lemul1a  12009  negiso  12136  xltneg  13146  lt2sq  14070  le2sq  14071  expmordi  14104  sqrtle  15197  prdsleval  17411  efgcpbllema  19700  iducn  24243  icopnfhmeo  24914  iccpnfhmeo  24916  xrhmeo  24917  reefiso  26431  sinord  26516  logltb  26582  logccv  26645  atanord  26910  birthdaylem3  26936  lgsquadlem3  27366  ltnegs  28058  oniso  28284  mddmd  32395  xrge0iifiso  34119  revwlkb  35348  erdszelem4  35416  erdszelem8  35420  satfv0  35580  cgrextend  36230  matunitlindf  37898  idlaut  40501  monotuz  43327  monotoddzzfi  43328  wepwsolem  43428  fnwe2val  43435  aomclem8  43447  isgrlim  48371  rrx2plord  49109  rrx2plordisom  49112