Theorem breqan12d 5101

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  breqan12rd  5102  soisores  7282  isoid  7284  isores3  7290  isoini2  7294  ofrfvalg  7639  fnwelem  8081  fnse  8083  infsupprpr  9419  wemaplem1  9461  r0weon  9934  sornom  10199  enqbreq2  10843  nqereu  10852  ordpinq  10866  lterpq  10893  ltresr2  11064  axpre-ltadd  11090  leltadd  11634  lemul1a  12009  negiso  12136  xltneg  13169  lt2sq  14095  le2sq  14096  expmordi  14129  sqrtle  15222  prdsleval  17440  efgcpbllema  19729  iducn  24247  icopnfhmeo  24910  iccpnfhmeo  24912  xrhmeo  24913  reefiso  26413  sinord  26498  logltb  26564  logccv  26627  atanord  26891  birthdaylem3  26917  lgsquadlem3  27345  ltnegs  28037  oniso  28263  mddmd  32372  xrge0iifiso  34079  revwlkb  35308  erdszelem4  35376  erdszelem8  35380  satfv0  35540  cgrextend  36190  matunitlindf  37939  idlaut  40542  monotuz  43369  monotoddzzfi  43370  wepwsolem  43470  fnwe2val  43477  aomclem8  43489  isgrlim  48458  rrx2plord  49196  rrx2plordisom  49199