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

Theorem dfvd2i 28653
Description: Inference form of dfvd2 28647. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
dfvd2i.1  |-  (. ph ,. ps  ->.  ch ).
Assertion
Ref Expression
dfvd2i  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem dfvd2i
StepHypRef Expression
1 dfvd2i.1 . 2  |-  (. ph ,. ps  ->.  ch ).
2 dfvd2 28647 . 2  |-  ( (.
ph ,. ps  ->.  ch ).  <->  ( ph  ->  ( ps  ->  ch ) ) )
31, 2mpbi 199 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28645
This theorem is referenced by:  vd23  28679  in2  28682  in2an  28685  gen21  28696  gen21nv  28697  gen22  28699  exinst  28701  exinst01  28702  exinst11  28703  e2  28708  e222  28713  e233  28854  e323  28855
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-an 360  df-vd2 28646
  Copyright terms: Public domain W3C validator