Metamath Proof Explorer

Theorem sbcim1

Description: Distribution of class substitution over implication. One direction of sbcimg that holds for proper classes. (Contributed by NM, 17-Aug-2018) Avoid ax-10 , ax-12 . (Revised by SN, 26-Oct-2024)

Ref Expression
Assertion sbcim1 ⊢ [˙A / x]˙ φ → ψ → [˙A / x]˙ φ → [˙A / x]˙ ψ

Proof

Step Hyp Ref Expression
1 sbcex ⊢ [˙A / x]˙ φ → ψ → A ∈ V
2 dfsbcq2 ⊢ y = A → y x φ → ψ ↔ [˙A / x]˙ φ → ψ
3 dfsbcq2 ⊢ y = A → y x φ ↔ [˙A / x]˙ φ
4 dfsbcq2 ⊢ y = A → y x ψ ↔ [˙A / x]˙ ψ
5 3 4 imbi12d ⊢ y = A → y x φ → y x ψ ↔ [˙A / x]˙ φ → [˙A / x]˙ ψ
6 2 5 imbi12d ⊢ y = A → y x φ → ψ → y x φ → y x ψ ↔ [˙A / x]˙ φ → ψ → [˙A / x]˙ φ → [˙A / x]˙ ψ
7 sbi1 ⊢ y x φ → ψ → y x φ → y x ψ
8 6 7 vtoclg ⊢ A ∈ V → [˙A / x]˙ φ → ψ → [˙A / x]˙ φ → [˙A / x]˙ ψ
9 1 8 mpcom ⊢ [˙A / x]˙ φ → ψ → [˙A / x]˙ φ → [˙A / x]˙ ψ