|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > wnor | Structured version Visualization version GIF version | ||
| Description: Extend wff definition to include joint denial ("nor"). | 
| Ref | Expression | 
|---|---|
| wph | wff 𝜑 | 
| wps | wff 𝜓 | 
| Ref | Expression | 
|---|---|
| wnor | wff (𝜑 ⊽ 𝜓) | 
| Colors of variables: wff setvar class | 
| Copyright terms: Public domain | W3C validator |