Metamath Proof Explorer


Theorem sbcimi

Description: Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)

Ref Expression
Hypotheses sbcimi.1 A V
sbcimi.2 [˙A / x]˙ φ χ
sbcimi.3 [˙A / x]˙ ψ η
Assertion sbcimi [˙A / x]˙ φ ψ χ η

Proof

Step Hyp Ref Expression
1 sbcimi.1 A V
2 sbcimi.2 [˙A / x]˙ φ χ
3 sbcimi.3 [˙A / x]˙ ψ η
4 sbcimg A V [˙A / x]˙ φ ψ [˙A / x]˙ φ [˙A / x]˙ ψ
5 1 4 ax-mp [˙A / x]˙ φ ψ [˙A / x]˙ φ [˙A / x]˙ ψ
6 2 3 imbi12i [˙A / x]˙ φ [˙A / x]˙ ψ χ η
7 5 6 bitri [˙A / x]˙ φ ψ χ η