Theorem breqan12d 4701

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   class class class wbr 4685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686

This theorem is referenced by:  breqan12rd  4702  soisores  6617  isoid  6619  isores3  6625  isoini2  6629  ofrfval  6947  fnwelem  7337  fnse  7339  wemaplem1  8492  r0weon  8873  sornom  9137  enqbreq2  9780  nqereu  9789  ordpinq  9803  lterpq  9830  ltresr2  10000  axpre-ltadd  10026  leltadd  10550  lemul1a  10915  negiso  11041  xltneg  12086  lt2sq  12977  le2sq  12978  sqrtle  14045  prdsleval  16184  efgcpbllema  18213  iducn  22134  icopnfhmeo  22789  iccpnfhmeo  22791  xrhmeo  22792  reefiso  24247  sinord  24325  logltb  24391  logccv  24454  atanord  24699  birthdaylem3  24725  lgsquadlem3  25152  mddmd  29288  xrge0iifiso  30109  erdszelem4  31302  erdszelem8  31306  cgrextend  32240  matunitlindf  33537  idlaut  35700  monotuz  37823  monotoddzzfi  37824  expmordi  37829  wepwsolem  37929  fnwe2val  37936  aomclem8  37948