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 605	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1562   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  breqan12rd  5119  soisores  7313  isoid  7315  isores3  7321  isoini2  7325  ofrfvalg  7670  fnwelem  8113  fnse  8115  infsupprpr  9454  wemaplem1  9496  r0weon  9970  sornom  10236  enqbreq2  10880  nqereu  10889  ordpinq  10903  lterpq  10930  ltresr2  11101  axpre-ltadd  11127  leltadd  11673  lemul1a  12047  negiso  12174  xltneg  13222  lt2sq  14148  le2sq  14149  expmordi  14182  sqrtle  15289  prdsleval  17508  efgcpbllema  19796  iducn  24344  icopnfhmeo  25007  iccpnfhmeo  25009  xrhmeo  25010  reefiso  26513  sinord  26601  logltb  26667  logccv  26730  atanord  26994  birthdaylem3  27020  lgsquadlem3  27448  ltnegs  28140  oniso  28366  mddmd  32506  xrge0iifiso  34234  revwlkb  35481  erdszelem4  35549  erdszelem8  35553  satfv0  35713  cgrextend  36363  matunitlindf  38122  idlaut  40725  monotuz  43523  monotoddzzfi  43524  wepwsolem  43624  fnwe2val  43631  aomclem8  43643  isgrlim  48609  rrx2plord  49347  rrx2plordisom  49350