Theorem frege 191

Description: Axiom 2 in the Metamath iset.mm database. This uses the other property of the positive exponential, which is that it can be duplicated.

Assertion

Ref	Expression
frege	⊦ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))

Proof of Theorem frege

Step	Hyp	Ref	Expression

Syntax hints:   → wim 180

 WARNING: This theorem has an incomplete proof.

This theorem is referenced by: (None)