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

Theorem vd01 28635
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 28601 1  |-  (. ps  ->.  ph ).
Colors of variables: wff set class
Syntax hints:   (.wvd1 28597
This theorem is referenced by:  e210  28697  e201  28699  e021  28703  e012  28705  e102  28707  e110  28714  e101  28716  e011  28718  e100  28720  e010  28722  e001  28724  e01  28729  e10  28732  sspwimpVD  28968
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 28598
  Copyright terms: Public domain W3C validator