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

Theorem dfvd2i 28677
Description: Inference form of dfvd2 28671. (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 28671 . 2  |-  ( (.
ph ,. ps  ->.  ch ).  <->  ( ph  ->  ( ps  ->  ch ) ) )
31, 2mpbi 200 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28669
This theorem is referenced by:  vd23  28703  in2  28706  in2an  28709  gen21  28720  gen21nv  28721  gen22  28723  exinst  28725  exinst01  28726  exinst11  28727  e2  28732  e222  28737  e233  28877  e323  28878
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-an 361  df-vd2 28670
  Copyright terms: Public domain W3C validator