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  9941  sornom  10206  enqbreq2  10849  nqereu  10858  ordpinq  10872  lterpq  10899  ltresr2  11070  axpre-ltadd  11096  leltadd  11638  lemul1a  12012  negiso  12139  xltneg  13153  lt2sq  14074  le2sq  14075  expmordi  14108  sqrtle  15202  prdsleval  17416  efgcpbllema  19668  iducn  24203  icopnfhmeo  24874  iccpnfhmeo  24876  xrhmeo  24877  reefiso  26391  sinord  26476  logltb  26542  logccv  26605  atanord  26870  birthdaylem3  26896  lgsquadlem3  27326  sltneg  27991  onsiso  28209  mddmd  32280  xrge0iifiso  33918  revwlkb  35106  erdszelem4  35174  erdszelem8  35178  satfv0  35338  cgrextend  35989  matunitlindf  37605  idlaut  40083  monotuz  42923  monotoddzzfi  42924  wepwsolem  43024  fnwe2val  43031  aomclem8  43043  isgrlim  47974  rrx2plord  48702  rrx2plordisom  48705