Theorem mtbid 662

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 653	1 |- ( ph -> -. ch )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnib  666  eqneltrrd  2261  neleqtrd  2262  eueq3dc  2895  efrirr  4325  fidcenumlemrks  6909  nqnq0pi  7370  zdclt  9259  xleaddadd  9814  frec2uzf1od  10331  expnegap0  10453  bcval5  10665  zfz1isolemiso  10738  seq3coll  10741  fisumss  11319  fprodssdc  11517  rpdvds  12010  oddpwdclemodd  12081  pceq0  12230  pcmpt  12250  pwle2  13712