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

Theorem hbxfrbi 1431
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 1429 . 2 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
41, 2, 33imtr4i 200 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wal 1312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  hbbi  1510  hb3or  1511  hb3an  1512  hbs1f  1737  hbs1  1889  hbsbv  1892  hbeu1  1985  sb8euh  1998  hbmo1  2013  hbmo  2014  hbab1  2104  hbab  2106  cleqh  2215  hbxfreq  2222  hbral  2439  hbra1  2440
  Copyright terms: Public domain W3C validator