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) Definition df-sb changed. (Revised by Wolf Lammen, 5-Jun-2026)

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

Proof

Step Hyp Ref Expression
1 sbi1lem ⊢ y x φ → ψ ∧ y x φ → ∀ u u = y → ∀ x x = u → ψ
2 sbi1lem ⊢ y x φ → ψ ∧ y x φ → ∀ z z = y → ∀ x x = z → ψ
3 df-sb ⊢ y x ψ ↔ ∀ u u = y → ∀ x x = u → ψ ∧ ∀ z z = y → ∀ x x = z → ψ
4 1 2 3 sylanbrc ⊢ y x φ → ψ ∧ y x φ → y x ψ
5 4 ex ⊢ y x φ → ψ → y x φ → y x ψ