Theorem breqan12d 5118

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  breqan12rd  5119  soisores  7335  isoid  7337  isores3  7343  isoini2  7347  ofrfvalg  7701  fnwelem  8143  fnwe2lem1  8145  fnse  8150  infsupprpr  9498  wemaplem1  9540  r0weon  10091  sornom  10355  enqbreq2  11005  nqereu  11014  ordpinq  11028  lterpq  11055  ltresr2  11226  axpre-ltadd  11252  leltadd  11800  lemul1a  12171  negiso  12297  xltneg  13347  lt2sq  14276  le2sq  14277  expmordi  14310  sqrtle  15427  prdsleval  17648  efgcpbllema  19968  matunitlindf  22996  iducn  24601  icopnfhmeo  25264  iccpnfhmeo  25266  xrhmeo  25267  reefiso  26775  sinord  26862  logltb  26928  logccv  26991  atanord  27255  birthdaylem3  27281  lgsquadlem3  27709  ltnegs  28431  oniso  28657  mddmd  32903  xrge0iifiso  34567  revwlkb  35908  erdszelem4  35959  erdszelem8  35963  satfv0  36123  cgrextend  36773  idlaut  41154  monotuz  43948  monotoddzzfi  43949  wepwsolem  44049  aomclem8  44063  hashomiso  46015  isgrlim  49080  rrx2plord  49832  rrx2plordisom  49835