Theorem hbxfrbi 1827

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2864 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 291	1 ⊢ (𝜑 → ∀𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539

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 206

This theorem is referenced by:  hbn1fw  2048  hbe1w  2051  hbe1  2139  hbsbw  2169  hbab1OLD  2719  hbab  2720  hbabg  2721  hbxfreq  2864  hbral  3305  bnj982  33784  bnj1095  33787  bnj1096  33788  bnj1276  33820  bnj594  33918  bnj1445  34050  hbra2VD  43611