Theorem mtbird 633

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 624	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 579  ax-in2 580

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  eqneltrd  2183  neleqtrrd  2186  fidifsnen  6586  php5fin  6598  tridc  6615  fimax2gtrilemstep  6616  en2eqpr  6623  inflbti  6719  addnidpig  6895  nqnq0pi  6997  ltpopr  7154  cauappcvgprlemladdru  7215  caucvgprlemladdrl  7237  caucvgprprlemnkltj  7248  caucvgprprlemnkeqj  7249  caucvgprprlemaddq  7267  ltposr  7309  axltirr  7553  reapirr  8054  apirr  8082  indstr2  9096  xrltnsym  9263  xrlttr  9265  xrltso  9266  lbioog  9331  ubioog  9332  fzn  9456  flqltnz  9694  iseqf1olemnab  9917  iseqf1olemqk  9923  exp3val  9957  zfz1isolemiso  10244  binomlem  10877  dvdsle  11123  2tp1odd  11162  divalglemeuneg  11201  bezoutlemle  11275  rpexp  11410  oddpwdclemxy  11425  oddpwdclemndvds  11427  sqpweven  11431  2sqpwodd  11432