Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wvd3 Structured version   Visualization version   Unicode version
Syntax Definition wvd3 38803
Description: Syntax for a 3-hypothesis virtual deduction. (New usage is discouraged.)
Hypotheses
Ref Expression
wph wff ph
wps wff ps
wch wff ch
wth wff th
Assertion
Ref Expression
wvd3 wff (. ph ,. ps ,. ch ->. th ).
See definition df-vd3 38806 for more information.
Colors of variables: wff setvar class
  Copyright terms: Public domain W3C validator