Metamath Proof Explorer

Theorem nn0indd

Description: Principle of Mathematical Induction (inference schema) on nonnegative integers, a deduction version. (Contributed by Thierry Arnoux, 23-Mar-2018)

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

Proof

Step	Hyp	Ref	Expression
1		nn0indd.1	$⊢ x = 0 \to (ψ \leftrightarrow χ)$
2		nn0indd.2	$⊢ x = y \to (ψ \leftrightarrow θ)$
3		nn0indd.3	$⊢ x = y + 1 \to (ψ \leftrightarrow τ)$
4		nn0indd.4	$⊢ x = A \to (ψ \leftrightarrow η)$
5		nn0indd.5	$⊢ φ \to χ$
6		nn0indd.6	$⊢ ((φ \land y \in ℕ_{0}) \land θ) \to τ$
7	1	imbi2d	$⊢ x = 0 \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 ℕ_{0}) \to (θ \to τ)$
12	11	expcom	$⊢ y \in ℕ_{0} \to (φ \to (θ \to τ))$
13	12	a2d	$⊢ y \in ℕ_{0} \to ((φ \to θ) \to (φ \to τ))$
14	7 8 9 10 5 13	nn0ind	$⊢ A \in ℕ_{0} \to (φ \to η)$
15	14	impcom	$⊢ (φ \land A \in ℕ_{0}) \to η$