Theorem breqan12d 5159

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  breqan12rd  5160  soisores  7347  isoid  7349  isores3  7355  isoini2  7359  ofrfvalg  7705  fnwelem  8156  fnse  8158  infsupprpr  9544  wemaplem1  9586  r0weon  10052  sornom  10317  enqbreq2  10960  nqereu  10969  ordpinq  10983  lterpq  11010  ltresr2  11181  axpre-ltadd  11207  leltadd  11747  lemul1a  12121  negiso  12248  xltneg  13259  lt2sq  14173  le2sq  14174  expmordi  14207  sqrtle  15299  prdsleval  17522  efgcpbllema  19772  iducn  24292  icopnfhmeo  24974  iccpnfhmeo  24976  xrhmeo  24977  reefiso  26492  sinord  26576  logltb  26642  logccv  26705  atanord  26970  birthdaylem3  26996  lgsquadlem3  27426  sltneg  28077  mddmd  32320  xrge0iifiso  33934  revwlkb  35131  erdszelem4  35199  erdszelem8  35203  satfv0  35363  cgrextend  36009  matunitlindf  37625  idlaut  40098  monotuz  42953  monotoddzzfi  42954  wepwsolem  43054  fnwe2val  43061  aomclem8  43073  isgrlim  47949  rrx2plord  48641  rrx2plordisom  48644