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

Theorem hbxfrbi 1341
 Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
hbxfrbi.1 (φψ)
hbxfrbi.2 (ψxψ)
Assertion
Ref Expression
hbxfrbi (φxφ)

Proof of Theorem hbxfrbi
StepHypRef Expression
1 hbxfrbi.2 . 2 (ψxψ)
2 hbxfrbi.1 . 2 (φψ)
32albii 1339 . 2 (xφxψ)
41, 2, 33imtr4i 190 1 (φxφ)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1226 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 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  hbbi  1422  hb3or  1423  hb3an  1424  hbs1f  1646  hbs1  1796  hbsbv  1799  hbeu1  1892  sb8euh  1905  hbmo1  1920  hbmo  1921  hbab1  2011  hbab  2013  cleqh  2119  hbxfreq  2126  hbral  2331  hbra1  2332
 Copyright terms: Public domain W3C validator