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

Theorem hbxfrbi 1361
 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 (𝜓 → ∀𝑥𝜓)
Assertion
Ref Expression
hbxfrbi (𝜑 → ∀𝑥𝜑)

Proof of Theorem hbxfrbi
StepHypRef Expression
1 hbxfrbi.2 . 2 (𝜓 → ∀𝑥𝜓)
2 hbxfrbi.1 . 2 (𝜑𝜓)
32albii 1359 . 2 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
41, 2, 33imtr4i 190 1 (𝜑 → ∀𝑥𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1241 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 1336  ax-gen 1338 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  hbbi  1440  hb3or  1441  hb3an  1442  hbs1f  1664  hbs1  1814  hbsbv  1817  hbeu1  1910  sb8euh  1923  hbmo1  1938  hbmo  1939  hbab1  2029  hbab  2031  cleqh  2137  hbxfreq  2144  hbral  2353  hbra1  2354
 Copyright terms: Public domain W3C validator