Metamath Proof Explorer

Theorem sbcim2g

Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg . sbcim2g is sbcim2gVD without virtual deductions and was automatically derived from sbcim2gVD using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbcim2g ⊢ A ∈ V → [˙A / x]˙ φ → ψ → χ ↔ [˙A / x]˙ φ → [˙A / x]˙ ψ → [˙A / x]˙ χ

Proof

Step Hyp Ref Expression
1 sbcimg ⊢ A ∈ V → [˙A / x]˙ φ → ψ → χ ↔ [˙A / x]˙ φ → [˙A / x]˙ ψ → χ
2 1 biimpd ⊢ A ∈ V → [˙A / x]˙ φ → ψ → χ → [˙A / x]˙ φ → [˙A / x]˙ ψ → χ
3 sbcimg ⊢ A ∈ V → [˙A / x]˙ ψ → χ ↔ [˙A / x]˙ ψ → [˙A / x]˙ χ
4 imbi2 ⊢ [˙A / x]˙ ψ → χ ↔ [˙A / x]˙ ψ → [˙A / x]˙ χ → [˙A / x]˙ φ → [˙A / x]˙ ψ → χ ↔ [˙A / x]˙ φ → [˙A / x]˙ ψ → [˙A / x]˙ χ
5 4 biimpcd ⊢ [˙A / x]˙ φ → [˙A / x]˙ ψ → χ → [˙A / x]˙ ψ → χ ↔ [˙A / x]˙ ψ → [˙A / x]˙ χ → [˙A / x]˙ φ → [˙A / x]˙ ψ → [˙A / x]˙ χ
6 2 3 5 syl6ci ⊢ A ∈ V → [˙A / x]˙ φ → ψ → χ → [˙A / x]˙ φ → [˙A / x]˙ ψ → [˙A / x]˙ χ
7 idd ⊢ A ∈ V → [˙A / x]˙ φ → [˙A / x]˙ ψ → [˙A / x]˙ χ → [˙A / x]˙ φ → [˙A / x]˙ ψ → [˙A / x]˙ χ
8 biimpr ⊢ [˙A / x]˙ ψ → χ ↔ [˙A / x]˙ ψ → [˙A / x]˙ χ → [˙A / x]˙ ψ → [˙A / x]˙ χ → [˙A / x]˙ ψ → χ
9 3 7 8 ee13 ⊢ A ∈ V → [˙A / x]˙ φ → [˙A / x]˙ ψ → [˙A / x]˙ χ → [˙A / x]˙ φ → [˙A / x]˙ ψ → χ
10 9 1 sylibrd ⊢ A ∈ V → [˙A / x]˙ φ → [˙A / x]˙ ψ → [˙A / x]˙ χ → [˙A / x]˙ φ → ψ → χ
11 6 10 impbid ⊢ A ∈ V → [˙A / x]˙ φ → ψ → χ ↔ [˙A / x]˙ φ → [˙A / x]˙ ψ → [˙A / x]˙ χ