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 ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) )

Proof

Step Hyp Ref Expression
1 sbcimg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) )
2 1 biimpd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) )
3 sbcimg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) )
4 imbi2 ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) )
5 4 biimpcd ⊢ ( ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) )
6 2 3 5 syl6ci ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) )
7 idd ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) )
8 biimpr ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) )
9 3 7 8 ee13 ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] ( 𝜓 → 𝜒 ) ) ) )
10 9 1 sylibrd ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) → [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) )
11 6 10 impbid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) ) ) )