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

Theorem breqan12d 5074
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 5063 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2an 595 1 ((𝜑𝜓) → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528   class class class wbr 5058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059
This theorem is referenced by:  breqan12rd  5075  soisores  7069  isoid  7071  isores3  7077  isoini2  7081  ofrfval  7406  fnwelem  7816  fnse  7818  infsupprpr  8957  wemaplem1  8999  r0weon  9427  sornom  9688  enqbreq2  10331  nqereu  10340  ordpinq  10354  lterpq  10381  ltresr2  10552  axpre-ltadd  10578  leltadd  11113  lemul1a  11483  negiso  11610  xltneg  12600  lt2sq  13488  le2sq  13489  expmordi  13521  sqrtle  14610  prdsleval  16740  efgcpbllema  18811  iducn  22821  icopnfhmeo  23476  iccpnfhmeo  23478  xrhmeo  23479  reefiso  24965  sinord  25045  logltb  25110  logccv  25173  atanord  25432  birthdaylem3  25459  lgsquadlem3  25886  mddmd  30006  xrge0iifiso  31078  revwlkb  32270  erdszelem4  32339  erdszelem8  32343  satfv0  32503  cgrextend  33367  matunitlindf  34772  idlaut  37114  monotuz  39418  monotoddzzfi  39419  wepwsolem  39522  fnwe2val  39529  aomclem8  39541  rrx2plord  44605  rrx2plordisom  44608
  Copyright terms: Public domain W3C validator