Theorem hbxfrbi 1822

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2870 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 1816	. 2 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)
4	1, 2, 3	3imtr4i 292	1 ⊢ (𝜑 → ∀𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  hbn1fw  2043  hbe1w  2046  hbe1  2141  hbsbwOLD  2170  hbab1OLD  2722  hbab  2723  hbabg  2724  hbxfreq  2870  hbral  3306  bnj982  34771  bnj1095  34774  bnj1096  34775  bnj1276  34807  bnj594  34905  bnj1445  35037  hbra2VD  44858