indstrd

Description: Strong induction, deduction version. (Contributed by Steven Nguyen, 13-Jul-2025)

	Ref	Expression
Hypotheses	indstrd.1	$⊢ x = y \to (ψ \leftrightarrow χ)$
	indstrd.2	$⊢ x = A \to (ψ \leftrightarrow θ)$
	indstrd.3	$⊢ (φ \land x \in ℕ \land \forall y \in ℕ (y < x \to χ)) \to ψ$
	indstrd.4	$⊢ φ \to A \in ℕ$
Assertion	indstrd	$⊢ φ \to θ$

Step	Hyp	Ref	Expression
1		indstrd.1	$⊢ x = y \to (ψ \leftrightarrow χ)$
2		indstrd.2	$⊢ x = A \to (ψ \leftrightarrow θ)$
3		indstrd.3	$⊢ (φ \land x \in ℕ \land \forall y \in ℕ (y < x \to χ)) \to ψ$
4		indstrd.4	$⊢ φ \to A \in ℕ$
5		eleq1	$⊢ x = A \to (x \in ℕ \leftrightarrow A \in ℕ)$
6	5 2	imbi12d	$⊢ x = A \to ((x \in ℕ \to ψ) \leftrightarrow (A \in ℕ \to θ))$
7	6	adantl	$⊢ (φ \land x = A) \to ((x \in ℕ \to ψ) \leftrightarrow (A \in ℕ \to θ))$
8	1	imbi2d	$⊢ x = y \to ((φ \to ψ) \leftrightarrow (φ \to χ))$
9		bi2.04	$⊢ (y < x \to (φ \to χ)) \leftrightarrow (φ \to (y < x \to χ))$
10	9	ralbii	$⊢ \forall y \in ℕ (y < x \to (φ \to χ)) \leftrightarrow \forall y \in ℕ (φ \to (y < x \to χ))$
11		r19.21v	$⊢ \forall y \in ℕ (φ \to (y < x \to χ)) \leftrightarrow (φ \to \forall y \in ℕ (y < x \to χ))$
12	10 11	bitri	$⊢ \forall y \in ℕ (y < x \to (φ \to χ)) \leftrightarrow (φ \to \forall y \in ℕ (y < x \to χ))$
13	3	3com12	$⊢ (x \in ℕ \land φ \land \forall y \in ℕ (y < x \to χ)) \to ψ$
14	13	3exp	$⊢ x \in ℕ \to (φ \to (\forall y \in ℕ (y < x \to χ) \to ψ))$
15	14	a2d	$⊢ x \in ℕ \to ((φ \to \forall y \in ℕ (y < x \to χ)) \to (φ \to ψ))$
16	12 15	biimtrid	$⊢ x \in ℕ \to (\forall y \in ℕ (y < x \to (φ \to χ)) \to (φ \to ψ))$
17	8 16	indstr	$⊢ x \in ℕ \to (φ \to ψ)$
18	17	com12	$⊢ φ \to (x \in ℕ \to ψ)$
19	4 7 18	vtocld	$⊢ φ \to (A \in ℕ \to θ)$
20	4 19	mpd	$⊢ φ \to θ$

Metamath Proof Explorer