Theorem hbxfrbi 1823

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2875 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 1817	. 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 1793  ax-4 1807

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  hbn1fw  2045  hbe1w  2048  hbe1  2143  hbsbwOLD  2173  hbab1OLD  2727  hbab  2728  hbabg  2729  hbxfreq  2875  hbral  3314  bnj982  34754  bnj1095  34757  bnj1096  34758  bnj1276  34790  bnj594  34888  bnj1445  35020  hbra2VD  44831