Theorem breqan12d 5182

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  breqan12rd  5183  soisores  7363  isoid  7365  isores3  7371  isoini2  7375  ofrfvalg  7722  fnwelem  8172  fnse  8174  infsupprpr  9573  wemaplem1  9615  r0weon  10081  sornom  10346  enqbreq2  10989  nqereu  10998  ordpinq  11012  lterpq  11039  ltresr2  11210  axpre-ltadd  11236  leltadd  11774  lemul1a  12148  negiso  12275  xltneg  13279  lt2sq  14183  le2sq  14184  expmordi  14217  sqrtle  15309  prdsleval  17537  efgcpbllema  19796  iducn  24313  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  reefiso  26510  sinord  26594  logltb  26660  logccv  26723  atanord  26988  birthdaylem3  27014  lgsquadlem3  27444  sltneg  28095  mddmd  32333  xrge0iifiso  33881  revwlkb  35093  erdszelem4  35162  erdszelem8  35166  satfv0  35326  cgrextend  35972  matunitlindf  37578  idlaut  40053  monotuz  42898  monotoddzzfi  42899  wepwsolem  42999  fnwe2val  43006  aomclem8  43018  isgrlim  47806  rrx2plord  48454  rrx2plordisom  48457