Theorem mtbid 661

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 652	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 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnib  665  eqneltrrd  2236  neleqtrd  2237  eueq3dc  2858  efrirr  4275  fidcenumlemrks  6841  nqnq0pi  7246  zdclt  9128  xleaddadd  9670  frec2uzf1od  10179  expnegap0  10301  bcval5  10509  zfz1isolemiso  10582  seq3coll  10585  fisumss  11161  rpdvds  11780  oddpwdclemodd  11850  pwle2  13193