Theorem breqan12d 5097

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

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

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082

This theorem is referenced by:  breqan12rd  5098  soisores  7230  isoid  7232  isores3  7238  isoini2  7242  ofrfvalg  7573  fnwelem  8003  fnse  8005  infsupprpr  9307  wemaplem1  9349  r0weon  9814  sornom  10079  enqbreq2  10722  nqereu  10731  ordpinq  10745  lterpq  10772  ltresr2  10943  axpre-ltadd  10969  leltadd  11505  lemul1a  11875  negiso  12001  xltneg  12997  lt2sq  13898  le2sq  13899  expmordi  13931  sqrtle  15017  prdsleval  17233  efgcpbllema  19405  iducn  23480  icopnfhmeo  24151  iccpnfhmeo  24153  xrhmeo  24154  reefiso  25652  sinord  25735  logltb  25800  logccv  25863  atanord  26122  birthdaylem3  26148  lgsquadlem3  26575  mddmd  30708  xrge0iifiso  31930  revwlkb  33132  erdszelem4  33201  erdszelem8  33205  satfv0  33365  cgrextend  34355  matunitlindf  35819  idlaut  38152  monotuz  40801  monotoddzzfi  40802  wepwsolem  40905  fnwe2val  40912  aomclem8  40924  rrx2plord  46124  rrx2plordisom  46127