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

Theorem breq123d 5067
Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
Hypotheses
Ref Expression
breq1d.1 (𝜑𝐴 = 𝐵)
breq123d.2 (𝜑𝑅 = 𝑆)
breq123d.3 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
breq123d (𝜑 → (𝐴𝑅𝐶𝐵𝑆𝐷))

Proof of Theorem breq123d
StepHypRef Expression
1 breq1d.1 . . 3 (𝜑𝐴 = 𝐵)
2 breq123d.3 . . 3 (𝜑𝐶 = 𝐷)
31, 2breq12d 5066 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
4 breq123d.2 . . 3 (𝜑𝑅 = 𝑆)
54breqd 5064 . 2 (𝜑 → (𝐵𝑅𝐷𝐵𝑆𝐷))
63, 5bitrd 282 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑆𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538   class class class wbr 5053
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-sn 4551  df-pr 4553  df-op 4557  df-br 5054
This theorem is referenced by:  sbcbr123  5107  fmptco  6880  xpsle  16850  invfuc  17242  yonedainv  17529  opphllem3  26541  lmif  26577  islmib  26579  iscgra  26601  isinag  26630  fmptcof2  30408  submomnd  30738  sgnsv  30829  inftmrel  30836  isinftm  30837  submarchi  30842  suborng  30915  uncov  34950  iscvlat  36531  paddfval  37005  lhpset  37203  tendofset  37966  diaffval  38238  fnwe2val  39849  aomclem8  39861  afv2eq12d  43637
  Copyright terms: Public domain W3C validator