Theorem mtbird 597

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 588	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  2130  neleqtrrd  2133  addnidpig  6320  nqnq0pi  6421  ltpopr  6569  cauappcvgprlemladdru  6628  caucvgprlemladdrl  6649  ltposr  6691  axltirr  6883  reapirr  7361  apirr  7389  indstr2  8322  xrltnsym  8484  xrlttr  8486  xrltso  8487  lbioog  8552  ubioog  8553  fzn  8676  expival  8911