Theorem breqan12d 4599

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  breqan12rd  4600  soisores  6477  isoid  6479  isores3  6485  isoini2  6489  ofrfval  6803  fnwelem  7179  fnse  7181  wemaplem1  8334  r0weon  8718  sornom  8982  enqbreq2  9621  nqereu  9630  ordpinq  9644  lterpq  9671  ltresr2  9841  axpre-ltadd  9867  leltadd  10391  lemul1a  10756  negiso  10880  xltneg  11922  lt2sq  12799  le2sq  12800  sqrtle  13849  prdsleval  15960  efgcpbllema  17990  iducn  21897  icopnfhmeo  22550  iccpnfhmeo  22552  xrhmeo  22553  reefiso  24006  sinord  24084  logltb  24150  logccv  24209  atanord  24454  birthdaylem3  24480  lgsquadlem3  24907  mddmd  28544  xrge0iifiso  29309  erdszelem4  30430  erdszelem8  30434  cgrextend  31285  matunitlindf  32577  idlaut  34400  monotuz  36524  monotoddzzfi  36525  expmordi  36530  wepwsolem  36630  fnwe2val  36637  aomclem8  36649