Theorem breqan12d 5119

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 5108	. 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 5103

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  breqan12rd  5120  soisores  7324  isoid  7326  isores3  7332  isoini2  7336  ofrfvalg  7685  fnwelem  8127  fnse  8129  infsupprpr  9476  wemaplem1  9518  r0weon  10048  sornom  10312  enqbreq2  10962  nqereu  10971  ordpinq  10985  lterpq  11012  ltresr2  11183  axpre-ltadd  11209  leltadd  11755  lemul1a  12126  negiso  12252  xltneg  13302  lt2sq  14230  le2sq  14231  expmordi  14264  sqrtle  15380  prdsleval  17595  efgcpbllema  19915  matunitlindf  22943  iducn  24548  icopnfhmeo  25211  iccpnfhmeo  25213  xrhmeo  25214  reefiso  26724  sinord  26811  logltb  26877  logccv  26940  atanord  27204  birthdaylem3  27230  lgsquadlem3  27658  ltnegs  28350  oniso  28576  mddmd  32822  xrge0iifiso  34486  revwlkb  35823  erdszelem4  35874  erdszelem8  35878  satfv0  36038  cgrextend  36689  idlaut  41067  monotuz  43880  monotoddzzfi  43881  wepwsolem  43981  fnwe2val  43988  aomclem8  44000  hashomiso  45946  isgrlim  48996  rrx2plord  49748  rrx2plordisom  49751