Theorem mtbird 663

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 653	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 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eqneltrd  2236  neleqtrrd  2239  fidifsnen  6772  php5fin  6784  tridc  6801  fimax2gtrilemstep  6802  en2eqpr  6809  inflbti  6919  omp1eomlem  6987  difinfsnlem  6992  addnidpig  7168  nqnq0pi  7270  ltpopr  7427  cauappcvgprlemladdru  7488  caucvgprlemladdrl  7510  caucvgprprlemnkltj  7521  caucvgprprlemnkeqj  7522  caucvgprprlemaddq  7540  ltposr  7595  axpre-suploclemres  7733  axltirr  7855  reapirr  8363  apirr  8391  indstr2  9430  xrltnsym  9609  xrlttr  9611  xrltso  9612  xltadd1  9689  xposdif  9695  xleaddadd  9700  lbioog  9726  ubioog  9727  fzn  9853  flqltnz  10091  iseqf1olemnab  10292  iseqf1olemqk  10298  exp3val  10326  zfz1isolemiso  10614  xrmaxltsup  11059  binomlem  11284  dvdsle  11578  2tp1odd  11617  divalglemeuneg  11656  bezoutlemle  11732  rpexp  11867  oddpwdclemxy  11883  oddpwdclemndvds  11885  sqpweven  11889  2sqpwodd  11890  ctinfom  11977  ivthinc  12829  logbgcd1irraplemexp  13093  neapmkvlem  13424