Theorem mtbid 644

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)

Hypotheses

Ref	Expression
mtbid.min	|- ( ph -> -. ps )
mtbid.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mtbid	|- ( ph -> -. ch )

Proof of Theorem mtbid

Step	Hyp	Ref	Expression
1		mtbid.min	. 2 |- ( ph -> -. ps )
2		mtbid.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimprd 157	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	mtod 635	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnib  648  eqneltrrd  2211  neleqtrd  2212  eueq3dc  2827  efrirr  4235  fidcenumlemrks  6793  nqnq0pi  7194  zdclt  9032  xleaddadd  9563  frec2uzf1od  10072  expnegap0  10194  bcval5  10402  zfz1isolemiso  10475  seq3coll  10478  fisumss  11053  rpdvds  11626  oddpwdclemodd  11695  pwle2  12885