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  4498  fidcenumlemrks  7270  2omap  7318  nqnq0pi  7805  zdclt  9726  xleaddadd  10299  qdclt  10690  frec2uzf1od  10856  expnegap0  10997  bcval5  11215  zfz1isolemiso  11305  seq3coll  11308  fisumss  12175  fprodssdc  12373  nninfctlemfo  12833  rpdvds  12893  nnmaxpwlemnfac  12967  pceq0  13121  pcmpt  13142  prmlem0  13240  gzsumfzval  13760  ply1termlem  15892  lgseisenlem1  16287  lgsquadlem3  16296  2sqlem8a  16339  2sqlem8  16340  pwle2  17126  stnot  17137  wexmiddifxylem  17143