Theorem mpt-P1.8 57

Description: Closed Form of Modus Ponens.

Assertion

Ref	Expression
mpt-P1.8	⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))

Proof of Theorem mpt-P1.8

Step	Hyp	Ref	Expression
1		id-P1.4 36	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓))
2	1	imcomm-P1.6.SH 49	1 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))

Syntax hints:   → wff-imp 10

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-MP 14

This theorem is referenced by:  mpt-P1.8.AC.2SH  58  mpt-P1.8.2AC.2SH  59  mpt-P1.8.3AC.2SH  60