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

Theorem 3brtr4d 3967
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 3949 . 2 (𝜑 → (𝐶𝑅𝐷𝐴𝑅𝐵))
51, 4mpbird 166 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332   class class class wbr 3936
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3079  df-sn 3537  df-pr 3538  df-op 3540  df-br 3937
This theorem is referenced by:  f1oiso2  5735  prarloclemarch2  7250  caucvgprprlemmu  7526  caucvgsrlembound  7625  mulap0  8438  lediv12a  8675  recp1lt1  8680  xleadd1a  9685  fldiv4p1lem1div2  10108  intfracq  10123  modqmulnn  10145  addmodlteq  10201  frecfzennn  10229  monoord2  10280  expgt1  10361  leexp2r  10377  leexp1a  10378  bernneq  10442  faclbnd  10518  faclbnd6  10521  facubnd  10522  hashunlem  10581  zfz1isolemiso  10613  sqrtgt0  10837  absrele  10886  absimle  10887  abstri  10907  abs2difabs  10911  bdtrilem  11041  bdtri  11042  xrmaxifle  11046  xrmaxadd  11061  xrbdtri  11076  climsqz  11135  climsqz2  11136  fsum3cvg2  11194  isumle  11295  expcnvap0  11302  expcnvre  11303  explecnv  11305  cvgratz  11332  efcllemp  11399  ege2le3  11412  eflegeo  11442  cos12dec  11508  phibnd  11927  psmetres2  12539  xmetres2  12585  comet  12705  bdxmet  12707  cnmet  12736  ivthdec  12828  limcimolemlt  12839  tangtx  12965  logbgcd1irraplemap  13092  cvgcmp2nlemabs  13400  trilpolemlt1  13407
  Copyright terms: Public domain W3C validator