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

Theorem breqan12d 4593
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 4582 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2an 492 1 ((𝜑𝜓) → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474   class class class wbr 4577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578
This theorem is referenced by:  breqan12rd  4594  soisores  6455  isoid  6457  isores3  6463  isoini2  6467  ofrfval  6781  fnwelem  7157  fnse  7159  wemaplem1  8312  r0weon  8696  sornom  8960  enqbreq2  9599  nqereu  9608  ordpinq  9622  lterpq  9649  ltresr2  9819  axpre-ltadd  9845  leltadd  10364  lemul1a  10729  negiso  10853  xltneg  11884  lt2sq  12757  le2sq  12758  sqrtle  13798  prdsleval  15909  efgcpbllema  17939  iducn  21845  icopnfhmeo  22498  iccpnfhmeo  22500  xrhmeo  22501  reefiso  23951  sinord  24029  logltb  24095  logccv  24154  atanord  24399  birthdaylem3  24425  lgsquadlem3  24852  mddmd  28378  xrge0iifiso  29143  erdszelem4  30264  erdszelem8  30268  cgrextend  31119  matunitlindf  32401  idlaut  34224  monotuz  36348  monotoddzzfi  36349  expmordi  36354  wepwsolem  36454  fnwe2val  36461  aomclem8  36473
  Copyright terms: Public domain W3C validator