Theorem breqan12d 5118

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  breqan12rd  5119  soisores  7284  isoid  7286  isores3  7292  isoini2  7296  ofrfvalg  7641  fnwelem  8087  fnse  8089  infsupprpr  9433  wemaplem1  9475  r0weon  9943  sornom  10208  enqbreq2  10851  nqereu  10860  ordpinq  10874  lterpq  10901  ltresr2  11072  axpre-ltadd  11098  leltadd  11640  lemul1a  12014  negiso  12141  xltneg  13155  lt2sq  14076  le2sq  14077  expmordi  14110  sqrtle  15203  prdsleval  17417  efgcpbllema  19669  iducn  24204  icopnfhmeo  24875  iccpnfhmeo  24877  xrhmeo  24878  reefiso  26392  sinord  26477  logltb  26543  logccv  26606  atanord  26871  birthdaylem3  26897  lgsquadlem3  27327  sltneg  27992  onsiso  28210  mddmd  32281  xrge0iifiso  33919  revwlkb  35107  erdszelem4  35175  erdszelem8  35179  satfv0  35339  cgrextend  35990  matunitlindf  37606  idlaut  40084  monotuz  42924  monotoddzzfi  42925  wepwsolem  43025  fnwe2val  43032  aomclem8  43044  isgrlim  47975  rrx2plord  48703  rrx2plordisom  48706