Theorem hbxfrbi 1826

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2881 for equality version. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
hbxfrbi.1	⊢ (𝜑 ↔ 𝜓)
hbxfrbi.2	⊢ (𝜓 → ∀𝑥𝜓)

Assertion

Ref	Expression
hbxfrbi	⊢ (𝜑 → ∀𝑥𝜑)

Proof of Theorem hbxfrbi

Step	Hyp	Ref	Expression
1		hbxfrbi.2	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2		hbxfrbi.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	2	albii 1821	. 2 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)
4	1, 2, 3	3imtr4i 295	1 ⊢ (𝜑 → ∀𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  hbn1fw  2052  hbe1w  2055  hbe1  2144  hbsbw  2173  hbab1  2743  hbab  2746  hbabg  2747  hbxfreq  2881  hbral  3149  bnj982  32278  bnj1095  32281  bnj1096  32282  bnj1276  32314  bnj594  32412  bnj1445  32544  hbra2VD  41939