Description: Alternate proof of sbn1 , not using the false constant. (Contributed by BJ, 18-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sbn1ALT | ⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 → ¬ [ 𝑡 / 𝑥 ] 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nsb | ⊢ ( ∀ 𝑥 ¬ ( 𝜑 ∧ ¬ 𝜑 ) → ¬ [ 𝑡 / 𝑥 ] ( 𝜑 ∧ ¬ 𝜑 ) ) | |
| 2 | pm3.24 | ⊢ ¬ ( 𝜑 ∧ ¬ 𝜑 ) | |
| 3 | 1 2 | mpg | ⊢ ¬ [ 𝑡 / 𝑥 ] ( 𝜑 ∧ ¬ 𝜑 ) |
| 4 | sban | ⊢ ( [ 𝑡 / 𝑥 ] ( 𝜑 ∧ ¬ 𝜑 ) ↔ ( [ 𝑡 / 𝑥 ] 𝜑 ∧ [ 𝑡 / 𝑥 ] ¬ 𝜑 ) ) | |
| 5 | 3 4 | mtbi | ⊢ ¬ ( [ 𝑡 / 𝑥 ] 𝜑 ∧ [ 𝑡 / 𝑥 ] ¬ 𝜑 ) |
| 6 | pm3.21 | ⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 → ( [ 𝑡 / 𝑥 ] 𝜑 → ( [ 𝑡 / 𝑥 ] 𝜑 ∧ [ 𝑡 / 𝑥 ] ¬ 𝜑 ) ) ) | |
| 7 | 5 6 | mtoi | ⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 → ¬ [ 𝑡 / 𝑥 ] 𝜑 ) |