Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wvd3 Unicode version

Syntax Definition wvd3 28533
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 28536 for more information.

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