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

Theorem vd01 28040
Description: A virtual hypothesis virtually infers a theorem. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
vd01.1  |-  ph
Assertion
Ref Expression
vd01  |-  (. ps  ->.  ph ).

Proof of Theorem vd01
StepHypRef Expression
1 vd01.1 . . 3  |-  ph
21a1i 11 . 2  |-  ( ps 
->  ph )
32dfvd1ir 28006 1  |-  (. ps  ->.  ph ).
Colors of variables: wff set class
Syntax hints:   (.wvd1 28002
This theorem is referenced by:  e210  28102  e201  28104  e021  28108  e012  28110  e102  28112  e110  28119  e101  28121  e011  28123  e100  28125  e010  28127  e001  28129  e01  28134  e10  28137  sspwimpVD  28373
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-vd1 28003
  Copyright terms: Public domain W3C validator