This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( 𝑥 = 0 → ( 𝜓 ↔ 𝜒 ) )
		nn0indd.2	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
		nn0indd.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜓 ↔ 𝜏 ) )
		nn0indd.4	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
		nn0indd.5	⊢ ( 𝜑 → 𝜒 )
		nn0indd.6	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ₀ ) ∧ 𝜃 ) → 𝜏 )
	Assertion	nn0indd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ₀ ) → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		nn0indd.1	⊢ ( 𝑥 = 0 → ( 𝜓 ↔ 𝜒 ) )
2		nn0indd.2	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
3		nn0indd.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜓 ↔ 𝜏 ) )
4		nn0indd.4	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
5		nn0indd.5	⊢ ( 𝜑 → 𝜒 )
6		nn0indd.6	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ₀ ) ∧ 𝜃 ) → 𝜏 )
7	1	imbi2d	⊢ ( 𝑥 = 0 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜒 ) ) )
8	2	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜃 ) ) )
9	3	imbi2d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜏 ) ) )
10	4	imbi2d	⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜂 ) ) )
11	6	ex	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ₀ ) → ( 𝜃 → 𝜏 ) )
12	11	expcom	⊢ ( 𝑦 ∈ ℕ₀ → ( 𝜑 → ( 𝜃 → 𝜏 ) ) )
13	12	a2d	⊢ ( 𝑦 ∈ ℕ₀ → ( ( 𝜑 → 𝜃 ) → ( 𝜑 → 𝜏 ) ) )
14	7 8 9 10 5 13	nn0ind	⊢ ( 𝐴 ∈ ℕ₀ → ( 𝜑 → 𝜂 ) )
15	14	impcom	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ₀ ) → 𝜂 )