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

Theorem dfvd2i 28354
Description: Inference form of dfvd2 28348. (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 28348 . 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 28346
This theorem is referenced by:  vd23  28374  in2  28377  in2an  28380  gen21  28391  gen21nv  28392  gen22  28394  exinst  28396  exinst01  28397  exinst11  28398  e2  28403  e222  28408  e233  28540  e323  28541
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 28347
  Copyright terms: Public domain W3C validator