Theorem mtbird 662

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-in1 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eqneltrd  2233  neleqtrrd  2236  fidifsnen  6757  php5fin  6769  tridc  6786  fimax2gtrilemstep  6787  en2eqpr  6794  inflbti  6904  omp1eomlem  6972  difinfsnlem  6977  addnidpig  7137  nqnq0pi  7239  ltpopr  7396  cauappcvgprlemladdru  7457  caucvgprlemladdrl  7479  caucvgprprlemnkltj  7490  caucvgprprlemnkeqj  7491  caucvgprprlemaddq  7509  ltposr  7564  axpre-suploclemres  7702  axltirr  7824  reapirr  8332  apirr  8360  indstr2  9396  xrltnsym  9572  xrlttr  9574  xrltso  9575  xltadd1  9652  xposdif  9658  xleaddadd  9663  lbioog  9689  ubioog  9690  fzn  9815  flqltnz  10053  iseqf1olemnab  10254  iseqf1olemqk  10260  exp3val  10288  zfz1isolemiso  10575  xrmaxltsup  11020  binomlem  11245  dvdsle  11531  2tp1odd  11570  divalglemeuneg  11609  bezoutlemle  11685  rpexp  11820  oddpwdclemxy  11836  oddpwdclemndvds  11838  sqpweven  11842  2sqpwodd  11843  ctinfom  11930  ivthinc  12779