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 ⊢φ→φ→ψ→φ→ψ