Theorem mtbird 630

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 142	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mtod 621	1 |- ( ph -> -. ps )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-in1 576  ax-in2 577

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  eqneltrd  2174  neleqtrrd  2177  fidifsnen  6355  php5fin  6366  en2eqpr  6380  inflbti  6437  addnidpig  6526  nqnq0pi  6628  ltpopr  6785  cauappcvgprlemladdru  6846  caucvgprlemladdrl  6868  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemaddq  6898  ltposr  6940  axltirr  7179  reapirr  7677  apirr  7705  indstr2  8696  xrltnsym  8868  xrlttr  8870  xrltso  8871  lbioog  8936  ubioog  8937  fzn  9061  flqltnz  9289  expival  9478  dvdsle  10244  2tp1odd  10284  divalglemeuneg  10323  bezoutlemle  10397  rpexp  10532  oddpwdclemxy  10547  oddpwdclemndvds  10549  sqpweven  10553  2sqpwodd  10554