ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3brtr3d GIF version

Theorem 3brtr3d 3929
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
3brtr3d.1 (𝜑𝐴𝑅𝐵)
3brtr3d.2 (𝜑𝐴 = 𝐶)
3brtr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3brtr3d (𝜑𝐶𝑅𝐷)

Proof of Theorem 3brtr3d
StepHypRef Expression
1 3brtr3d.1 . 2 (𝜑𝐴𝑅𝐵)
2 3brtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
3 3brtr3d.3 . . 3 (𝜑𝐵 = 𝐷)
42, 3breq12d 3912 . 2 (𝜑 → (𝐴𝑅𝐵𝐶𝑅𝐷))
51, 4mpbid 146 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316   class class class wbr 3899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900
This theorem is referenced by:  ofrval  5960  phplem2  6715  ltaddnq  7183  prarloclemarch2  7195  prmuloclemcalc  7341  axcaucvglemcau  7674  apreap  8317  ltmul1  8322  subap0d  8374  divap1d  8529  div2subap  8564  lemul2a  8585  mul2lt0rlt0  9514  xleadd2a  9625  monoord2  10218  expubnd  10318  bernneq2  10381  resqrexlemcalc2  10755  resqrexlemcalc3  10756  abs2dif2  10847  bdtrilem  10978  bdtri  10979  xrmaxaddlem  10997  fsum00  11199  iserabs  11212  geosergap  11243  mertenslemi1  11272  eftlub  11323  eirraplem  11410  xblss2  12501  xmstri2  12566  mstri2  12567  xmstri  12568  mstri  12569  xmstri3  12570  mstri3  12571  msrtri  12572
  Copyright terms: Public domain W3C validator