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

Theorem vd01 28431
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 10 . 2  |-  ( ps 
->  ph )
32dfvd1ir 28397 1  |-  (. ps  ->.  ph ).
Colors of variables: wff set class
Syntax hints:   (.wvd1 28393
This theorem is referenced by:  e210  28493  e201  28495  e021  28499  e012  28501  e102  28503  e110  28510  e101  28512  e011  28514  e100  28516  e010  28518  e001  28520  e01  28525  e10  28529  sspwimpVD  28768
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 177  df-vd1 28394
  Copyright terms: Public domain W3C validator