Theorem mtbird 598

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)

Hypotheses

Ref	Expression
mtbird.min	|- ( ph -> -. ch )
mtbird.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mtbird	|- ( ph -> -. ps )

Proof of Theorem mtbird

Step	Hyp	Ref	Expression
1		mtbird.min	. 2 |- ( ph -> -. ch )
2		mtbird.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimpd 132	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mtod 589	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-in1 544  ax-in2 545

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  eqneltrd  2133  neleqtrrd  2136  fidifsnen  6331  php5fin  6339  addnidpig  6434  nqnq0pi  6536  ltpopr  6693  cauappcvgprlemladdru  6754  caucvgprlemladdrl  6776  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemaddq  6806  ltposr  6848  axltirr  7086  reapirr  7568  apirr  7596  indstr2  8546  xrltnsym  8714  xrlttr  8716  xrltso  8717  lbioog  8782  ubioog  8783  fzn  8906  flqltnz  9129  expival  9257