Theorem breqan12d 5165

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  breqan12rd  5166  soisores  7324  isoid  7326  isores3  7332  isoini2  7336  ofrfvalg  7678  fnwelem  8117  fnse  8119  infsupprpr  9499  wemaplem1  9541  r0weon  10007  sornom  10272  enqbreq2  10915  nqereu  10924  ordpinq  10938  lterpq  10965  ltresr2  11136  axpre-ltadd  11162  leltadd  11698  lemul1a  12068  negiso  12194  xltneg  13196  lt2sq  14098  le2sq  14099  expmordi  14132  sqrtle  15207  prdsleval  17423  efgcpbllema  19622  iducn  23788  icopnfhmeo  24459  iccpnfhmeo  24461  xrhmeo  24462  reefiso  25960  sinord  26043  logltb  26108  logccv  26171  atanord  26432  birthdaylem3  26458  lgsquadlem3  26885  sltneg  27519  mddmd  31554  xrge0iifiso  32915  revwlkb  34116  erdszelem4  34185  erdszelem8  34189  satfv0  34349  cgrextend  34980  matunitlindf  36486  idlaut  38967  monotuz  41680  monotoddzzfi  41681  wepwsolem  41784  fnwe2val  41791  aomclem8  41803  rrx2plord  47406  rrx2plordisom  47409