Metamath Proof Explorer

Theorem minimp-pm2.43

Description: Derivation of pm2.43 (also called "hilbert" or W) from ax-mp and minimp . It uses the classical derivation from ax-1 and ax-2 written DD22D21 in D-notation (see head comment for an explanation) and shortens the proof using mp2 (which only requires ax-mp ). (Contributed by BJ, 31-May-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion minimp-pm2.43 ⊢ φ → φ → ψ → φ → ψ

Proof

Step Hyp Ref Expression
1 minimp-ax2 ⊢ φ → φ → ψ → φ → φ → φ → ψ
2 minimp-ax1 ⊢ φ → φ → ψ → φ
3 minimp-ax2 ⊢ φ → φ → ψ → φ → φ → φ → ψ → φ → φ
4 2 3 ax-mp ⊢ φ → φ → ψ → φ → φ
5 minimp-ax2 ⊢ φ → φ → ψ → φ → φ → φ → ψ → φ → φ → ψ → φ → φ → φ → φ → ψ → φ → ψ
6 1 4 5 mp2 ⊢ φ → φ → ψ → φ → ψ