Metamath Proof Explorer

Theorem sbi1ALT

Description: Alternate proof of sbt , shorter but using additional axioms. (Contributed by NM, 14-May-1993) Remove dependencies on axioms. (Revised by Steven Nguyen, 24-Jul-2023) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion sbi1ALT ⊢ y x φ → ψ → y x φ → y x ψ

Proof

Step Hyp Ref Expression
1 dfsb ⊢ y x φ → ψ ↔ ∀ z z = y → ∀ x x = z → φ → ψ
2 ax-2 ⊢ x = z → φ → ψ → x = z → φ → x = z → ψ
3 2 al2imi ⊢ ∀ x x = z → φ → ψ → ∀ x x = z → φ → ∀ x x = z → ψ
4 3 imim3i ⊢ z = y → ∀ x x = z → φ → ψ → z = y → ∀ x x = z → φ → z = y → ∀ x x = z → ψ
5 4 al2imi ⊢ ∀ z z = y → ∀ x x = z → φ → ψ → ∀ z z = y → ∀ x x = z → φ → ∀ z z = y → ∀ x x = z → ψ
6 dfsb ⊢ y x φ ↔ ∀ z z = y → ∀ x x = z → φ
7 dfsb ⊢ y x ψ ↔ ∀ z z = y → ∀ x x = z → ψ
8 5 6 7 3imtr4g ⊢ ∀ z z = y → ∀ x x = z → φ → ψ → y x φ → y x ψ
9 1 8 sylbi ⊢ y x φ → ψ → y x φ → y x ψ