cbv1

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See cbv1v with disjoint variable conditions, not depending on ax-13 . (Contributed by NM, 5-Aug-1993) (Revised by Mario Carneiro, 3-Oct-2016) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbv1.1	$⊢ Ⅎ x φ$
	cbv1.2	$⊢ Ⅎ y φ$
	cbv1.3	$⊢ φ \to Ⅎ y ψ$
	cbv1.4	$⊢ φ \to Ⅎ x χ$
	cbv1.5	$⊢ φ \to (x = y \to (ψ \to χ))$
Assertion	cbv1	$⊢ φ \to (\forall x ψ \to \forall y χ)$

Proof

Step	Hyp	Ref	Expression
1		cbv1.1	$⊢ Ⅎ x φ$
2		cbv1.2	$⊢ Ⅎ y φ$
3		cbv1.3	$⊢ φ \to Ⅎ y ψ$
4		cbv1.4	$⊢ φ \to Ⅎ x χ$
5		cbv1.5	$⊢ φ \to (x = y \to (ψ \to χ))$
6	2 3	nfim1	$⊢ Ⅎ y (φ \to ψ)$
7	1 4	nfim1	$⊢ Ⅎ x (φ \to χ)$
8	5	com12	$⊢ x = y \to (φ \to (ψ \to χ))$
9	8	a2d	$⊢ x = y \to ((φ \to ψ) \to (φ \to χ))$
10	6 7 9	cbv3	$⊢ \forall x (φ \to ψ) \to \forall y (φ \to χ)$
11	1	19.21	$⊢ \forall x (φ \to ψ) \leftrightarrow (φ \to \forall x ψ)$
12	2	19.21	$⊢ \forall y (φ \to χ) \leftrightarrow (φ \to \forall y χ)$
13	10 11 12	3imtr3i	$⊢ (φ \to \forall x ψ) \to (φ \to \forall y χ)$
14	13	pm2.86i	$⊢ φ \to (\forall x ψ \to \forall y χ)$

Metamath Proof Explorer

Theorem cbv1

Proof