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

Theorem hbxfrbi 1406
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 1404 . 2 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
41, 2, 33imtr4i 199 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wal 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  hbbi  1485  hb3or  1486  hb3an  1487  hbs1f  1711  hbs1  1862  hbsbv  1865  hbeu1  1958  sb8euh  1971  hbmo1  1986  hbmo  1987  hbab1  2077  hbab  2079  cleqh  2187  hbxfreq  2194  hbral  2407  hbra1  2408
  Copyright terms: Public domain W3C validator