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 t x ¬ φ ¬ t x φ

Proof

Step Hyp Ref Expression
1 nsb x ¬ ¬ t x
2 fal ¬
3 1 2 mpg ¬ t x
4 pm2.21 ¬ φ φ
5 4 sb2imi t x ¬ φ t x φ t x
6 3 5 mtoi t x ¬ φ ¬ t x φ