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

Theorem hbxfrbi 1377
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 1375 . 2 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
41, 2, 33imtr4i 194 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102  wal 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  hbbi  1456  hb3or  1457  hb3an  1458  hbs1f  1680  hbs1  1830  hbsbv  1833  hbeu1  1926  sb8euh  1939  hbmo1  1954  hbmo  1955  hbab1  2045  hbab  2047  cleqh  2153  hbxfreq  2160  hbral  2370  hbra1  2371
  Copyright terms: Public domain W3C validator