Theorem hbxfrbi 1826

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2919 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  2784  hbab  2787  hbabg  2788  hbxfreq  2919  hbral  3185  bnj982  32160  bnj1095  32163  bnj1096  32164  bnj1276  32196  bnj594  32294  bnj1445  32426  hbra2VD  41566