Theorem adh-minimp-pm2.43 43334

Description: Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minimp-ax1 43328, adh-minimp-ax2 43332, and ax-mp 5. It uses the derivation written DD22D21 in D-notation. (See head comment for an explanation.) Polish prefix notation: CCpCpqCpq . (Contributed by BJ, 31-May-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
adh-minimp-pm2.43	⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))

Proof of Theorem adh-minimp-pm2.43

Step	Hyp	Ref	Expression
1		adh-minimp-ax1 43328	. . 3 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜑))
2		adh-minimp-ax2 43332	. . 3 ⊢ ((𝜑 → ((𝜑 → 𝜓) → 𝜑)) → ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜑)))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜑))
4		adh-minimp-ax2 43332	. . 3 ⊢ ((𝜑 → (𝜑 → 𝜓)) → ((𝜑 → 𝜑) → (𝜑 → 𝜓)))
5		adh-minimp-ax2 43332	. . 3 ⊢ (((𝜑 → (𝜑 → 𝜓)) → ((𝜑 → 𝜑) → (𝜑 → 𝜓))) → (((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜑)) → ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))))
6	4, 5	ax-mp 5	. 2 ⊢ (((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜑)) → ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓)))
7	3, 6	ax-mp 5	1 ⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by: (None)