Syntax Definition wi 4

Description: If 𝜑 and 𝜓 are wff's, so is (𝜑 → 𝜓) or "𝜑 implies 𝜓". Part of the recursive definition of a wff. The left-hand wff is called the antecedent, and the right-hand wff is called the consequent. In the case of (𝜑 → (𝜓 → 𝜒)), the middle 𝜓 may be informally called either an antecedent or part of the consequent depending on context.

Hypotheses

Ref	Expression
wph	wff 𝜑
wps	wff 𝜓

Assertion

Ref	Expression
wi	wff (𝜑 → 𝜓)

This syntax is primitive. The first axiom using it is ax-1 6.