Theorem breqan12d 5123

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  breqan12rd  5124  soisores  7302  isoid  7304  isores3  7310  isoini2  7314  ofrfvalg  7661  fnwelem  8110  fnse  8112  infsupprpr  9457  wemaplem1  9499  r0weon  9965  sornom  10230  enqbreq2  10873  nqereu  10882  ordpinq  10896  lterpq  10923  ltresr2  11094  axpre-ltadd  11120  leltadd  11662  lemul1a  12036  negiso  12163  xltneg  13177  lt2sq  14098  le2sq  14099  expmordi  14132  sqrtle  15226  prdsleval  17440  efgcpbllema  19684  iducn  24170  icopnfhmeo  24841  iccpnfhmeo  24843  xrhmeo  24844  reefiso  26358  sinord  26443  logltb  26509  logccv  26572  atanord  26837  birthdaylem3  26863  lgsquadlem3  27293  sltneg  27951  onsiso  28169  mddmd  32230  xrge0iifiso  33925  revwlkb  35113  erdszelem4  35181  erdszelem8  35185  satfv0  35345  cgrextend  35996  matunitlindf  37612  idlaut  40090  monotuz  42930  monotoddzzfi  42931  wepwsolem  43031  fnwe2val  43038  aomclem8  43050  isgrlim  47981  rrx2plord  48709  rrx2plordisom  48712