Metamath Proof Explorer


Theorem bnj1096

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1096.1 ( 𝜑 → ∀ 𝑥 𝜑 )
bnj1096.2 ( 𝜓 ↔ ( 𝜒𝜃𝜏𝜑 ) )
Assertion bnj1096 ( 𝜓 → ∀ 𝑥 𝜓 )

Proof

Step Hyp Ref Expression
1 bnj1096.1 ( 𝜑 → ∀ 𝑥 𝜑 )
2 bnj1096.2 ( 𝜓 ↔ ( 𝜒𝜃𝜏𝜑 ) )
3 ax-5 ( 𝜒 → ∀ 𝑥 𝜒 )
4 ax-5 ( 𝜃 → ∀ 𝑥 𝜃 )
5 ax-5 ( 𝜏 → ∀ 𝑥 𝜏 )
6 3 4 5 1 bnj982 ( ( 𝜒𝜃𝜏𝜑 ) → ∀ 𝑥 ( 𝜒𝜃𝜏𝜑 ) )
7 2 6 hbxfrbi ( 𝜓 → ∀ 𝑥 𝜓 )