Theorem mtbid 673

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 664	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnib  677  eqneltrrd  2293  neleqtrd  2294  eueq3dc  2938  efrirr  4388  fidcenumlemrks  7019  nqnq0pi  7505  zdclt  9403  xleaddadd  9962  qdclt  10335  frec2uzf1od  10498  expnegap0  10639  bcval5  10855  zfz1isolemiso  10931  seq3coll  10934  fisumss  11557  fprodssdc  11755  nninfctlemfo  12207  rpdvds  12267  oddpwdclemodd  12340  pceq0  12491  pcmpt  12512  gsumfzval  13034  ply1termlem  14978  lgseisenlem1  15311  lgsquadlem3  15320  2sqlem8a  15363  2sqlem8  15364  pwle2  15643