Theorem mtbid 679

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 158	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	mtod 669	1 |- ( ph -> -. ch )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnib  683  eqneltrrd  2329  neleqtrd  2330  eueq3dc  2990  efrirr  4473  fidcenumlemrks  7222  2omap  7268  nqnq0pi  7752  zdclt  9654  xleaddadd  10219  qdclt  10604  frec2uzf1od  10767  expnegap0  10908  bcval5  11124  zfz1isolemiso  11207  seq3coll  11210  fisumss  12074  fprodssdc  12272  nninfctlemfo  12732  rpdvds  12792  oddpwdclemodd  12865  pceq0  13016  pcmpt  13037  gsumfzval  13596  ply1termlem  15599  lgseisenlem1  15935  lgsquadlem3  15944  2sqlem8a  15987  2sqlem8  15988  pwle2  16764