Theorem breqan12d 5108

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

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

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  breqan12rd  5109  soisores  7264  isoid  7266  isores3  7272  isoini2  7276  ofrfvalg  7621  fnwelem  8064  fnse  8066  infsupprpr  9396  wemaplem1  9438  r0weon  9906  sornom  10171  enqbreq2  10814  nqereu  10823  ordpinq  10837  lterpq  10864  ltresr2  11035  axpre-ltadd  11061  leltadd  11604  lemul1a  11978  negiso  12105  xltneg  13119  lt2sq  14040  le2sq  14041  expmordi  14074  sqrtle  15167  prdsleval  17381  efgcpbllema  19633  iducn  24168  icopnfhmeo  24839  iccpnfhmeo  24841  xrhmeo  24842  reefiso  26356  sinord  26441  logltb  26507  logccv  26570  atanord  26835  birthdaylem3  26861  lgsquadlem3  27291  sltneg  27958  onsiso  28176  mddmd  32249  xrge0iifiso  33918  revwlkb  35119  erdszelem4  35187  erdszelem8  35191  satfv0  35351  cgrextend  36002  matunitlindf  37618  idlaut  40095  monotuz  42934  monotoddzzfi  42935  wepwsolem  43035  fnwe2val  43042  aomclem8  43054  isgrlim  47986  rrx2plord  48725  rrx2plordisom  48728