Theorem adh-minimp-idALT 44378

Description: Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minimp-ax1 44373, adh-minimp-ax2 44377, and ax-mp 5. It uses the derivation written DD211 in D-notation. (See head comment for an explanation.) Polish prefix notation: Cpp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
adh-minimp-idALT	⊢ (𝜑 → 𝜑)

Proof of Theorem adh-minimp-idALT

Step	Hyp	Ref	Expression
1		adh-minimp-ax1 44373	. 2 ⊢ (𝜑 → (𝜓 → 𝜑))
2		adh-minimp-ax1 44373	. . 3 ⊢ (𝜑 → ((𝜓 → 𝜑) → 𝜑))
3		adh-minimp-ax2 44377	. . 3 ⊢ ((𝜑 → ((𝜓 → 𝜑) → 𝜑)) → ((𝜑 → (𝜓 → 𝜑)) → (𝜑 → 𝜑)))
4	2, 3	ax-mp 5	. 2 ⊢ ((𝜑 → (𝜓 → 𝜑)) → (𝜑 → 𝜑))
5	1, 4	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)