New Foundations Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > NFE Home > Th. List > wi  Unicode version 
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 lefthand wff is called the antecedent, and the righthand 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. 
Ref  Expression 

wph  
wps 
Ref  Expression 

wi 
Colors of variables: wff set class 
Copyright terms: Public domain  W3C validator 