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

Theorem 3brtr4d 3841
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 3824 . 2 (𝜑 → (𝐶𝑅𝐷𝐴𝑅𝐵))
51, 4mpbird 165 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285   class class class wbr 3811
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-v 2614  df-un 2988  df-sn 3428  df-pr 3429  df-op 3431  df-br 3812
This theorem is referenced by:  f1oiso2  5545  prarloclemarch2  6881  caucvgprprlemmu  7157  caucvgsrlembound  7242  mulap0  8021  lediv12a  8249  recp1lt1  8254  fldiv4p1lem1div2  9601  intfracq  9616  modqmulnn  9638  addmodlteq  9694  frecfzennn  9722  monoord2  9771  expgt1  9830  leexp2r  9846  leexp1a  9847  bernneq  9909  faclbnd  9984  faclbnd6  9987  facubnd  9988  hashunlem  10047  sqrtgt0  10294  absrele  10343  absimle  10344  abstri  10364  abs2difabs  10368  climsqz  10547  climsqz2  10548  phibnd  10973
  Copyright terms: Public domain W3C validator