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

Theorem hbxfrbi 1358
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 1356 . 2 (xφxψ)
41, 2, 33imtr4i 190 1 (φxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wal 1240
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 1333  ax-gen 1335
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  hbbi  1437  hb3or  1438  hb3an  1439  hbs1f  1661  hbs1  1811  hbsbv  1814  hbeu1  1907  sb8euh  1920  hbmo1  1935  hbmo  1936  hbab1  2026  hbab  2028  cleqh  2134  hbxfreq  2141  hbral  2347  hbra1  2348
  Copyright terms: Public domain W3C validator