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