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

Theorem breqtri 4068
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
breqtr.1 𝐴𝑅𝐵
breqtr.2 𝐵 = 𝐶
Assertion
Ref Expression
breqtri 𝐴𝑅𝐶

Proof of Theorem breqtri
StepHypRef Expression
1 breqtr.1 . 2 𝐴𝑅𝐵
2 breqtr.2 . . 3 𝐵 = 𝐶
32breq2i 4051 . 2 (𝐴𝑅𝐵𝐴𝑅𝐶)
41, 3mpbi 145 1 𝐴𝑅𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1372   class class class wbr 4043
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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044
This theorem is referenced by:  breqtrri  4070  3brtr3i  4072  le9lt10  9529  9lt10  9633  sqrt2gt1lt2  11331  trireciplem  11782  cos1bnd  12041  cos2bnd  12042  cos01gt0  12045  sin4lt0  12049  z4even  12198  dec2dvds  12705  coseq00topi  15278  sincos4thpi  15283  lgsdir2lem2  15477  lgsdir2lem3  15478  ex-fl  15623
  Copyright terms: Public domain W3C validator