Theorem hbxfrbi 1495

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  hbbi  1571  hb3or  1572  hb3an  1573  hbs1f  1804  hbs1  1966  hbsbv  1969  hbeu1  2064  sb8euh  2077  hbmo1  2092  hbmo  2093  hbab1  2194  hbab  2196  cleqh  2305  hbxfreq  2312  hbral  2535  hbra1  2536