Theorem hbxfrbi 1828

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

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

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  hbn1fw  2049  hbe1w  2052  hbe1  2140  hbsbw  2170  hbab1OLD  2720  hbab  2721  hbabg  2722  hbxfreq  2865  hbral  3306  bnj982  33789  bnj1095  33792  bnj1096  33793  bnj1276  33825  bnj594  33923  bnj1445  34055  hbra2VD  43621