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

Theorem hbc 110
Description: Hypothesis builder for combination. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
hbc.1 F:(βγ)
hbc.2 A:β
hbc.3 B:α
hbc.4 R⊧[(λx:α FB) = F]
hbc.5 R⊧[(λx:α AB) = A]
Assertion
Ref Expression
hbc R⊧[(λx:α (FA)B) = (FA)]

Proof of Theorem hbc
StepHypRef Expression
1 hbc.1 . . . . 5 F:(βγ)
2 hbc.2 . . . . 5 A:β
31, 2wc 50 . . . 4 (FA):γ
43wl 66 . . 3 λx:α (FA):(αγ)
5 hbc.3 . . 3 B:α
64, 5wc 50 . 2 (λx:α (FA)B):γ
7 hbc.4 . . . 4 R⊧[(λx:α FB) = F]
87ax-cb1 29 . . 3 R:∗
91, 2, 5distrc 93 . . 3 ⊤⊧[(λx:α (FA)B) = ((λx:α FB)(λx:α AB))]
108, 9a1i 28 . 2 R⊧[(λx:α (FA)B) = ((λx:α FB)(λx:α AB))]
111wl 66 . . . 4 λx:α F:(α → (βγ))
1211, 5wc 50 . . 3 (λx:α FB):(βγ)
13 hbc.5 . . . 4 R⊧[(λx:α AB) = A]
142, 13eqtypri 81 . . 3 (λx:α AB):β
1512, 14, 7, 13ceq12 88 . 2 R⊧[((λx:α FB)(λx:α AB)) = (FA)]
166, 10, 15eqtri 95 1 R⊧[(λx:α (FA)B) = (FA)]
Colors of variables: type var term
Syntax hints:  ht 2  kc 5  λkl 6   = ke 7  [kbr 9  wffMMJ2 11  wffMMJ2t 12
This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-wc 49  ax-ceq 51  ax-wl 65  ax-distrc 68  ax-wov 71  ax-eqtypi 77  ax-eqtypri 80
This theorem depends on definitions:  df-ov 73
This theorem is referenced by:  hbov  111  clf  115  exlimdv  167  cbvf  179  leqf  181  exlimd  183  alimdv  184  eximdv  185  alnex  186  exmid  199  ax5  207  ax6  208  ax7  209  ax9  212  axext  219  axrep  220
  Copyright terms: Public domain W3C validator