Theorem breqan12d 5102

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  breqan12rd  5103  soisores  7277  isoid  7279  isores3  7285  isoini2  7289  ofrfvalg  7634  fnwelem  8076  fnse  8078  infsupprpr  9414  wemaplem1  9456  r0weon  9929  sornom  10194  enqbreq2  10838  nqereu  10847  ordpinq  10861  lterpq  10888  ltresr2  11059  axpre-ltadd  11085  leltadd  11629  lemul1a  12004  negiso  12131  xltneg  13164  lt2sq  14090  le2sq  14091  expmordi  14124  sqrtle  15217  prdsleval  17435  efgcpbllema  19724  iducn  24261  icopnfhmeo  24924  iccpnfhmeo  24926  xrhmeo  24927  reefiso  26430  sinord  26515  logltb  26581  logccv  26644  atanord  26908  birthdaylem3  26934  lgsquadlem3  27363  ltnegs  28055  oniso  28281  mddmd  32391  xrge0iifiso  34099  revwlkb  35328  erdszelem4  35396  erdszelem8  35400  satfv0  35560  cgrextend  36210  matunitlindf  37959  idlaut  40562  monotuz  43393  monotoddzzfi  43394  wepwsolem  43494  fnwe2val  43501  aomclem8  43513  isgrlim  48476  rrx2plord  49214  rrx2plordisom  49217