Theorem hbxfrbi 1828

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

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

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  hbn1fw  2049  hbe1w  2052  hbe1  2141  hbsbw  2171  hbab1OLD  2725  hbab  2726  hbabg  2727  hbxfreq  2868  hbral  3144  bnj982  32658  bnj1095  32661  bnj1096  32662  bnj1276  32694  bnj594  32792  bnj1445  32924  hbra2VD  42369