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\in \mathrm{V}$$
	sbcimi.2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \chi$$
	sbcimi.3	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \eta$$
Assertion	sbcimi	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \to \psi \right)\leftrightarrow \left(\chi \to \eta \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcimi.1	$$⊢A\in \mathrm{V}$$
2		sbcimi.2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \chi$$
3		sbcimi.3	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \eta$$
4		sbcimg	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \to \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)\right)$$
5	1 4	ax-mp	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \to \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
6	2 3	imbi12i	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\chi \to \eta \right)$$
7	5 6	bitri	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \to \psi \right)\leftrightarrow \left(\chi \to \eta \right)$$