Theorem mtbid 667

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 658	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 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnib  671  eqneltrrd  2267  neleqtrd  2268  eueq3dc  2904  efrirr  4336  fidcenumlemrks  6928  nqnq0pi  7393  zdclt  9282  xleaddadd  9837  frec2uzf1od  10355  expnegap0  10477  bcval5  10690  zfz1isolemiso  10767  seq3coll  10770  fisumss  11348  fprodssdc  11546  rpdvds  12046  oddpwdclemodd  12119  pceq0  12268  pcmpt  12288  2sqlem8a  13717  2sqlem8  13718  pwle2  13996