Theorem syl6eqbr 2657

Description: A chained equality inference for a binary relation.

Hypotheses

Ref	Expression
syl6eqbr.1	|- (ph -> A = B)
syl6eqbr.2	|- BRC

Assertion

Ref	Expression
syl6eqbr	|- (ph -> ARC)

Proof of Theorem syl6eqbr

Step	Hyp	Ref	Expression
1		syl6eqbr.2	. 2 |- BRC
2		syl6eqbr.1	. . 3 |- (ph -> A = B)
3	2	breq1d 2634	. 2 |- (ph -> (ARC <-> BRC))
4	1, 3	mpbiri 194	1 |- (ph -> ARC)

Syntax hints:   -> wi 3   = wceq 958   class class class wbr 2624

This theorem is referenced by:  syl6eqbrr 2658  mapdom2 4500  unifiOLD 4570  fodomfi 4575  fodomfiOLD 4576  pm54.43 4581  expmwordit 6607  exple1t 6608  seq1bnd 6910  facwordit 6944  faclbnd3 6947  bcpasc 6969  efcltlem2 7305  ruclem27 7537  nmosetn0 8424  nmo0 8447  siii 8509  bcsALT 9041  occllem5 9172  branmfnt 10033

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2053  df-sn 2416  df-pr 2417  df-op 2420  df-br 2625

Copyright terms: Public domain