Theorem breqan12d 5105

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-sn 4573  df-pr 4575  df-op 4579  df-br 5090

This theorem is referenced by:  breqan12rd  5106  soisores  7248  isoid  7250  isores3  7256  isoini2  7260  ofrfvalg  7595  fnwelem  8031  fnse  8033  infsupprpr  9353  wemaplem1  9395  r0weon  9861  sornom  10126  enqbreq2  10769  nqereu  10778  ordpinq  10792  lterpq  10819  ltresr2  10990  axpre-ltadd  11016  leltadd  11552  lemul1a  11922  negiso  12048  xltneg  13044  lt2sq  13945  le2sq  13946  expmordi  13978  sqrtle  15063  prdsleval  17277  efgcpbllema  19447  iducn  23533  icopnfhmeo  24204  iccpnfhmeo  24206  xrhmeo  24207  reefiso  25705  sinord  25788  logltb  25853  logccv  25916  atanord  26175  birthdaylem3  26201  lgsquadlem3  26628  mddmd  30892  xrge0iifiso  32124  revwlkb  33327  erdszelem4  33396  erdszelem8  33400  satfv0  33560  cgrextend  34401  matunitlindf  35873  idlaut  38357  monotuz  41014  monotoddzzfi  41015  wepwsolem  41118  fnwe2val  41125  aomclem8  41137  rrx2plord  46406  rrx2plordisom  46409