Syntax Definition wi 2

Description: If φ and ψ are wff's, so is (φ → ψ) or "φ implies ψ." Part of the recursive definition of a wff. The resulting wff is (interpreted as) false when φ is true and ψ is false; it is true otherwise. (Think of the truth table for an OR gate with input φ connected through an inverter.) 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 3.

metamath.org