Theorem breqan12d 5094

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1541   class class class wbr 5078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079

This theorem is referenced by:  breqan12rd  5095  soisores  7191  isoid  7193  isores3  7199  isoini2  7203  ofrfvalg  7532  fnwelem  7956  fnse  7958  infsupprpr  9224  wemaplem1  9266  r0weon  9752  sornom  10017  enqbreq2  10660  nqereu  10669  ordpinq  10683  lterpq  10710  ltresr2  10881  axpre-ltadd  10907  leltadd  11442  lemul1a  11812  negiso  11938  xltneg  12933  lt2sq  13833  le2sq  13834  expmordi  13866  sqrtle  14953  prdsleval  17169  efgcpbllema  19341  iducn  23416  icopnfhmeo  24087  iccpnfhmeo  24089  xrhmeo  24090  reefiso  25588  sinord  25671  logltb  25736  logccv  25799  atanord  26058  birthdaylem3  26084  lgsquadlem3  26511  mddmd  30642  xrge0iifiso  31864  revwlkb  33066  erdszelem4  33135  erdszelem8  33139  satfv0  33299  cgrextend  34289  matunitlindf  35754  idlaut  38089  monotuz  40743  monotoddzzfi  40744  wepwsolem  40847  fnwe2val  40854  aomclem8  40866  rrx2plord  46018  rrx2plordisom  46021