Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > wi  Structured version Unicode version 
Description: If and are wff's, so is or " implies ." Part of the recursive definition of a wff. 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 