Metamath Proof Explorer

Theorem nnindd

Description: Principle of Mathematical Induction (inference schema) on integers, a deduction version. (Contributed by Thierry Arnoux, 19-Jul-2020)

		Ref	Expression
	Hypotheses	nnindd.1	$⊢ x = 1 \to (ψ \leftrightarrow χ)$
		nnindd.2	$⊢ x = y \to (ψ \leftrightarrow θ)$
		nnindd.3	$⊢ x = y + 1 \to (ψ \leftrightarrow τ)$
		nnindd.4	$⊢ x = A \to (ψ \leftrightarrow η)$
		nnindd.5	$⊢ φ \to χ$
		nnindd.6	$⊢ ((φ \land y \in ℕ) \land θ) \to τ$
	Assertion	nnindd	$⊢ (φ \land A \in ℕ) \to η$

Proof

Step	Hyp	Ref	Expression
1		nnindd.1	$⊢ x = 1 \to (ψ \leftrightarrow χ)$
2		nnindd.2	$⊢ x = y \to (ψ \leftrightarrow θ)$
3		nnindd.3	$⊢ x = y + 1 \to (ψ \leftrightarrow τ)$
4		nnindd.4	$⊢ x = A \to (ψ \leftrightarrow η)$
5		nnindd.5	$⊢ φ \to χ$
6		nnindd.6	$⊢ ((φ \land y \in ℕ) \land θ) \to τ$
7	1	imbi2d	$⊢ x = 1 \to ((φ \to ψ) \leftrightarrow (φ \to χ))$
8	2	imbi2d	$⊢ x = y \to ((φ \to ψ) \leftrightarrow (φ \to θ))$
9	3	imbi2d	$⊢ x = y + 1 \to ((φ \to ψ) \leftrightarrow (φ \to τ))$
10	4	imbi2d	$⊢ x = A \to ((φ \to ψ) \leftrightarrow (φ \to η))$
11	6	ex	$⊢ (φ \land y \in ℕ) \to (θ \to τ)$
12	11	expcom	$⊢ y \in ℕ \to (φ \to (θ \to τ))$
13	12	a2d	$⊢ y \in ℕ \to ((φ \to θ) \to (φ \to τ))$
14	7 8 9 10 5 13	nnind	$⊢ A \in ℕ \to (φ \to η)$
15	14	impcom	$⊢ (φ \land A \in ℕ) \to η$