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

Theorem syl5eqr 2068
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5eqr.1 B = A
syl5eqr.2 (φB = 𝐶)
Assertion
Ref Expression
syl5eqr (φA = 𝐶)

Proof of Theorem syl5eqr
StepHypRef Expression
1 syl5eqr.1 . . 3 B = A
21eqcomi 2026 . 2 A = B
3 syl5eqr.2 . 2 (φB = 𝐶)
42, 3syl5eq 2066 1 (φA = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  3eqtr3g  2077  csbeq1a  2837  ssdifeq0  3282  pofun  4023  opabbi2dv  4412  funimaexg  4909  fresin  4993  f1imacnv  5068  foimacnv  5069  fsn2  5262  fmptpr  5280  funiunfvdm  5327  funiunfvdmf  5328  fcof1o  5354  f1opw2  5629  fnexALT  5663  eqerlem  6048  mul02  6970
  Copyright terms: Public domain W3C validator