Theorem simp 190

Description: Principle of simplification. Allows discarding an unneeded antecedent. This is not possible with linear implication, since such a move would be non-linear; the ! exponentials in the definition of the logical implication operator allow 𝜓 to be discarded. Axiom 1 in the Metamath iset.mm database.

Assertion

Ref	Expression
simp	⊦ (𝜑 → (𝜓 → 𝜑))

Proof of Theorem simp

Step	Hyp	Ref	Expression

Syntax hints:   → wim 180

 WARNING: This theorem has an incomplete proof.

This theorem is referenced by: (None)