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

Theorem breq123d 4592
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 4591 . 2 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
4 breq123d.2 . . 3 (𝜑𝑅 = 𝑆)
54breqd 4589 . 2 (𝜑 → (𝐵𝑅𝐷𝐵𝑆𝐷))
63, 5bitrd 267 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑆𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475   class class class wbr 4578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4579
This theorem is referenced by:  sbcbr123  4631  fmptco  6288  xpsle  16013  invfuc  16406  yonedainv  16693  opphllem3  25387  lmif  25423  islmib  25425  iscgra  25447  isinag  25475  fmptcof2  28633  submomnd  28835  sgnsv  28852  inftmrel  28859  isinftm  28860  submarchi  28865  suborng  28940  uncov  32354  iscvlat  33422  paddfval  33895  lhpset  34093  tendofset  34858  diaffval  35131  fnwe2val  36431  aomclem8  36443
  Copyright terms: Public domain W3C validator