Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  breqan12d Structured version   Visualization version   GIF version

Theorem breqan12d 5047
 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
StepHypRef Expression
1 breq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 breqan12i.2 . 2 (𝜓𝐶 = 𝐷)
3 breq12 5036 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2an 598 1 ((𝜑𝜓) → (𝐴𝑅𝐶𝐵𝑅𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   class class class wbr 5031 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5032 This theorem is referenced by:  breqan12rd  5048  soisores  7064  isoid  7066  isores3  7072  isoini2  7076  ofrfval  7403  fnwelem  7815  fnse  7817  infsupprpr  8959  wemaplem1  9001  r0weon  9430  sornom  9695  enqbreq2  10338  nqereu  10347  ordpinq  10361  lterpq  10388  ltresr2  10559  axpre-ltadd  10585  leltadd  11120  lemul1a  11490  negiso  11615  xltneg  12605  lt2sq  13501  le2sq  13502  expmordi  13534  sqrtle  14619  prdsleval  16749  efgcpbllema  18880  iducn  22903  icopnfhmeo  23562  iccpnfhmeo  23564  xrhmeo  23565  reefiso  25057  sinord  25140  logltb  25205  logccv  25268  atanord  25527  birthdaylem3  25553  lgsquadlem3  25980  mddmd  30098  xrge0iifiso  31324  revwlkb  32521  erdszelem4  32590  erdszelem8  32594  satfv0  32754  cgrextend  33618  matunitlindf  35095  idlaut  37432  monotuz  39946  monotoddzzfi  39947  wepwsolem  40050  fnwe2val  40057  aomclem8  40069  rrx2plord  45193  rrx2plordisom  45196
 Copyright terms: Public domain W3C validator