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  9722  xleaddadd  10289  qdclt  10680  frec2uzf1od  10843  expnegap0  10984  bcval5  11201  zfz1isolemiso  11291  seq3coll  11294  fisumss  12159  fprodssdc  12357  nninfctlemfo  12817  rpdvds  12877  oddpwdclemodd  12950  pceq0  13101  pcmpt  13122  gzsumfzval  13711  ply1termlem  15843  lgseisenlem1  16189  lgsquadlem3  16198  2sqlem8a  16241  2sqlem8  16242  pwle2  17028  stnot  17039  wexmiddifxylem  17045