Theorem mtbid 683

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

This proof depends on syntax axioms:   -. wn 3   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylnib  687  eqneltrrd  2335  neleqtrd  2336  eueq3dc  3000  efrirr  4500  fidcenumlemrks  7277  2omap  7324  nqnq0pi  7811  zdclt  9731  xleaddadd  10305  qdclt  10696  frec2uzf1od  10863  expnegap0  11004  bcval5  11222  zfz1isolemiso  11312  seq3coll  11315  fisumss  12183  fprodssdc  12381  nninfctlemfo  12841  rpdvds  12901  nnmaxpwlemnfac  12975  pceq0  13129  pcmpt  13150  prmlem0  13248  gzsumfzval  13769  ply1termlem  15985  lgseisenlem1  16411  lgsquadlem3  16420  2sqlem8a  16463  2sqlem8  16464  pwle2  17250  stnot  17261  wexmiddifxylem  17267