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  2290  neleqtrd  2291  eueq3dc  2935  efrirr  4385  fidcenumlemrks  7014  nqnq0pi  7500  zdclt  9397  xleaddadd  9956  qdclt  10318  frec2uzf1od  10480  expnegap0  10621  bcval5  10837  zfz1isolemiso  10913  seq3coll  10916  fisumss  11538  fprodssdc  11736  nninfctlemfo  12180  rpdvds  12240  oddpwdclemodd  12313  pceq0  12463  pcmpt  12484  gsumfzval  12977  ply1termlem  14921  lgseisenlem1  15227  lgsquadlem3  15236  2sqlem8a  15279  2sqlem8  15280  pwle2  15559