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

Metamath Proof Explorer

Theorem sbi1

Description: Distribute substitution over implication. (Contributed by NM, 14-May-1993) Remove dependencies on axioms. (Revised by Steven Nguyen, 24-Jul-2023)

Ref Expression
Assertion sbi1 ⊢ 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 ψ