Theorem breqan12d 5104

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

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

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 3393  df-v 3435  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5089

This theorem is referenced by:  breqan12rd  5105  soisores  7255  isoid  7257  isores3  7263  isoini2  7267  ofrfvalg  7612  fnwelem  8055  fnse  8057  infsupprpr  9384  wemaplem1  9426  r0weon  9894  sornom  10159  enqbreq2  10802  nqereu  10811  ordpinq  10825  lterpq  10852  ltresr2  11023  axpre-ltadd  11049  leltadd  11592  lemul1a  11966  negiso  12093  xltneg  13107  lt2sq  14028  le2sq  14029  expmordi  14062  sqrtle  15154  prdsleval  17368  efgcpbllema  19620  iducn  24151  icopnfhmeo  24822  iccpnfhmeo  24824  xrhmeo  24825  reefiso  26339  sinord  26424  logltb  26490  logccv  26553  atanord  26818  birthdaylem3  26844  lgsquadlem3  27274  sltneg  27941  onsiso  28159  mddmd  32232  xrge0iifiso  33916  revwlkb  35116  erdszelem4  35184  erdszelem8  35188  satfv0  35348  cgrextend  35999  matunitlindf  37615  idlaut  40092  monotuz  42931  monotoddzzfi  42932  wepwsolem  43032  fnwe2val  43039  aomclem8  43051  isgrlim  47980  rrx2plord  48719  rrx2plordisom  48722