Theorem hbxfrbi 1824

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

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

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  hbn1fw  2044  hbe1w  2047  hbe1  2142  hbsbwOLD  2171  hbab1OLD  2723  hbab  2724  hbabg  2725  hbxfreq  2871  hbral  3307  bnj982  34793  bnj1095  34796  bnj1096  34797  bnj1276  34829  bnj594  34927  bnj1445  35059  hbra2VD  44885