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  4389  fidcenumlemrks  7028  nqnq0pi  7524  zdclt  9422  xleaddadd  9981  qdclt  10354  frec2uzf1od  10517  expnegap0  10658  bcval5  10874  zfz1isolemiso  10950  seq3coll  10953  fisumss  11576  fprodssdc  11774  nninfctlemfo  12234  rpdvds  12294  oddpwdclemodd  12367  pceq0  12518  pcmpt  12539  gsumfzval  13095  ply1termlem  15086  lgseisenlem1  15419  lgsquadlem3  15428  2sqlem8a  15471  2sqlem8  15472  2omap  15750  pwle2  15753