Theorem breqan12d 5163

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148

This theorem is referenced by:  breqan12rd  5164  soisores  7346  isoid  7348  isores3  7354  isoini2  7358  ofrfvalg  7704  fnwelem  8154  fnse  8156  infsupprpr  9541  wemaplem1  9583  r0weon  10049  sornom  10314  enqbreq2  10957  nqereu  10966  ordpinq  10980  lterpq  11007  ltresr2  11178  axpre-ltadd  11204  leltadd  11744  lemul1a  12118  negiso  12245  xltneg  13255  lt2sq  14169  le2sq  14170  expmordi  14203  sqrtle  15295  prdsleval  17523  efgcpbllema  19786  iducn  24307  icopnfhmeo  24987  iccpnfhmeo  24989  xrhmeo  24990  reefiso  26506  sinord  26590  logltb  26656  logccv  26719  atanord  26984  birthdaylem3  27010  lgsquadlem3  27440  sltneg  28091  mddmd  32329  xrge0iifiso  33895  revwlkb  35109  erdszelem4  35178  erdszelem8  35182  satfv0  35342  cgrextend  35989  matunitlindf  37604  idlaut  40078  monotuz  42929  monotoddzzfi  42930  wepwsolem  43030  fnwe2val  43037  aomclem8  43049  isgrlim  47884  rrx2plord  48569  rrx2plordisom  48572