This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbn1

Description: One direction of sbn , using fewer axioms. Compare 19.2 . (Contributed by Steven Nguyen, 18-Aug-2023)

Ref Expression
Assertion sbn1 ( [ 𝑡 / 𝑥 ] ¬ 𝜑 → ¬ [ 𝑡 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 nsb ⊢ ( ∀ 𝑥 ¬ ⊥ → ¬ [ 𝑡 / 𝑥 ] ⊥ )
2 fal ⊢ ¬ ⊥
3 1 2 mpg ⊢ ¬ [ 𝑡 / 𝑥 ] ⊥
4 pm2.21 ⊢ ( ¬ 𝜑 → ( 𝜑 → ⊥ ) )
5 4 sb2imi ⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 → ( [ 𝑡 / 𝑥 ] 𝜑 → [ 𝑡 / 𝑥 ] ⊥ ) )
6 3 5 mtoi ⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 → ¬ [ 𝑡 / 𝑥 ] 𝜑 )