HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ceq1 Unicode version

Theorem ceq1 79
Description: Equality theorem for combination.
Hypotheses
Ref Expression
ceq12.1 |- F:(al -> be)
ceq12.2 |- A:al
ceq12.3 |- R |= [F = T]
Assertion
Ref Expression
ceq1 |- R |= [(FA) = (TA)]

Proof of Theorem ceq1
StepHypRef Expression
1 ceq12.1 . 2 |- F:(al -> be)
2 ceq12.2 . 2 |- A:al
3 ceq12.3 . 2 |- R |= [F = T]
43ax-cb1 29 . . 3 |- R:*
54, 2eqid 73 . 2 |- R |= [A = A]
61, 2, 3, 5ceq12 78 1 |- R |= [(FA) = (TA)]
Colors of variables: type var term
Syntax hints:   -> ht 2  kc 5   = ke 7  [kbr 9   |= wffMMJ2 11  wffMMJ2t 12
This theorem is referenced by:  hbxfrf  97  ovl  107  alval  132  exval  133  euval  134  notval  135  ax4g  139  dfan2  144  eta  166  ac  184  ax14  204  axrep  207  axpow  208  axun  209
This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-refl 39  ax-eqmp 42  ax-ceq 46
This theorem depends on definitions:  df-ov 65
  Copyright terms: Public domain W3C validator