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

Theorem 3brtr3d 4031
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 4013 . 2 (𝜑 → (𝐴𝑅𝐵𝐶𝑅𝐷))
51, 4mpbid 147 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353   class class class wbr 4000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600  df-br 4001
This theorem is referenced by:  ofrval  6086  phplem2  6846  ltaddnq  7384  prarloclemarch2  7396  prmuloclemcalc  7542  axcaucvglemcau  7875  apreap  8521  ltmul1  8526  divap1d  8734  div2subap  8770  lemul2a  8792  mul2lt0rlt0  9733  xleadd2a  9848  monoord2  10450  expubnd  10550  bernneq2  10614  nn0ltexp2  10661  apexp1  10669  resqrexlemcalc2  10995  resqrexlemcalc3  10996  abs2dif2  11087  bdtrilem  11218  bdtri  11219  xrmaxaddlem  11239  fsum00  11441  iserabs  11454  geosergap  11485  mertenslemi1  11514  eftlub  11669  eirraplem  11755  unitmulcl  13094  unitgrp  13097  xblss2  13538  xmstri2  13603  mstri2  13604  xmstri  13605  mstri  13606  xmstri3  13607  mstri3  13608  msrtri  13609  logdivlti  13935  2sqlem8  14092  apdifflemr  14418
  Copyright terms: Public domain W3C validator