Theorem mtbid 662

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 653	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 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnib  666  eqneltrrd  2263  neleqtrd  2264  eueq3dc  2900  efrirr  4331  fidcenumlemrks  6918  nqnq0pi  7379  zdclt  9268  xleaddadd  9823  frec2uzf1od  10341  expnegap0  10463  bcval5  10676  zfz1isolemiso  10752  seq3coll  10755  fisumss  11333  fprodssdc  11531  rpdvds  12031  oddpwdclemodd  12104  pceq0  12253  pcmpt  12273  2sqlem8a  13598  2sqlem8  13599  pwle2  13878