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

Theorem 3brtr4d 3897
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
Hypotheses
Ref Expression
3brtr4d.1 (𝜑𝐴𝑅𝐵)
3brtr4d.2 (𝜑𝐶 = 𝐴)
3brtr4d.3 (𝜑𝐷 = 𝐵)
Assertion
Ref Expression
3brtr4d (𝜑𝐶𝑅𝐷)

Proof of Theorem 3brtr4d
StepHypRef Expression
1 3brtr4d.1 . 2 (𝜑𝐴𝑅𝐵)
2 3brtr4d.2 . . 3 (𝜑𝐶 = 𝐴)
3 3brtr4d.3 . . 3 (𝜑𝐷 = 𝐵)
42, 3breq12d 3880 . 2 (𝜑 → (𝐶𝑅𝐷𝐴𝑅𝐵))
51, 4mpbird 166 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1296   class class class wbr 3867
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475  df-br 3868
This theorem is referenced by:  f1oiso2  5644  prarloclemarch2  7075  caucvgprprlemmu  7351  caucvgsrlembound  7436  mulap0  8220  lediv12a  8452  recp1lt1  8457  xleadd1a  9439  fldiv4p1lem1div2  9861  intfracq  9876  modqmulnn  9898  addmodlteq  9954  frecfzennn  9982  monoord2  10027  expgt1  10108  leexp2r  10124  leexp1a  10125  bernneq  10189  faclbnd  10264  faclbnd6  10267  facubnd  10268  hashunlem  10327  zfz1isolemiso  10359  sqrtgt0  10582  absrele  10631  absimle  10632  abstri  10652  abs2difabs  10656  bdtrilem  10785  bdtri  10786  xrmaxifle  10789  xrmaxadd  10804  xrbdtri  10819  climsqz  10878  climsqz2  10879  fsum3cvg2  10937  isumle  11038  expcnvap0  11045  expcnvre  11046  explecnv  11048  cvgratz  11075  efcllemp  11097  ege2le3  11110  eflegeo  11141  phibnd  11620  psmetres2  12119  xmetres2  12165  comet  12285  bdxmet  12287  cnmet  12309
  Copyright terms: Public domain W3C validator