Theorem breqan12d 5123

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   class class class wbr 5107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  breqan12rd  5124  soisores  7331  isoid  7333  isores3  7339  isoini2  7343  ofrfvalg  7689  fnwelem  8132  fnse  8134  infsupprpr  9479  wemaplem1  9521  r0weon  10018  sornom  10282  enqbreq2  10932  nqereu  10941  ordpinq  10955  lterpq  10982  ltresr2  11153  axpre-ltadd  11179  leltadd  11725  lemul1a  12096  negiso  12222  xltneg  13271  lt2sq  14199  le2sq  14200  expmordi  14233  sqrtle  15349  prdsleval  17566  efgcpbllema  19882  matunitlindf  22904  iducn  24509  icopnfhmeo  25172  iccpnfhmeo  25174  xrhmeo  25175  reefiso  26681  sinord  26769  logltb  26835  logccv  26898  atanord  27162  birthdaylem3  27188  lgsquadlem3  27616  ltnegs  28308  oniso  28534  mddmd  32768  xrge0iifiso  34432  revwlkb  35709  erdszelem4  35760  erdszelem8  35764  satfv0  35924  cgrextend  36575  idlaut  40956  monotuz  43769  monotoddzzfi  43770  wepwsolem  43870  fnwe2val  43877  aomclem8  43889  hashomiso  45835  isgrlim  48885  rrx2plord  49637  rrx2plordisom  49640