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  2261  neleqtrrd  2264  eqnbrtrd  3999  fidifsnen  6832  php5fin  6844  tridc  6861  fimax2gtrilemstep  6862  en2eqpr  6869  inflbti  6985  omp1eomlem  7055  difinfsnlem  7060  addnidpig  7273  nqnq0pi  7375  ltpopr  7532  cauappcvgprlemladdru  7593  caucvgprlemladdrl  7615  caucvgprprlemnkltj  7626  caucvgprprlemnkeqj  7627  caucvgprprlemaddq  7645  ltposr  7700  axpre-suploclemres  7838  axltirr  7961  reapirr  8471  apirr  8499  indstr2  9543  xrltnsym  9725  xrlttr  9727  xrltso  9728  xltadd1  9808  xposdif  9814  xleaddadd  9819  lbioog  9845  ubioog  9846  fzn  9973  flqltnz  10218  iseqf1olemnab  10419  iseqf1olemqk  10425  exp3val  10453  zfz1isolemiso  10748  xrmaxltsup  11195  binomlem  11420  dvdsle  11778  2tp1odd  11817  divalglemeuneg  11856  bezoutlemle  11937  rpexp  12081  oddpwdclemxy  12097  oddpwdclemndvds  12099  sqpweven  12103  2sqpwodd  12104  oddprm  12187  pythagtriplem11  12202  pythagtriplem13  12204  pcpremul  12221  pczndvds2  12245  pc2dvds  12257  pcmpt  12269  ctinfom  12357  ivthinc  13221  logbgcd1irraplemexp  13486  lgsval2lem  13511  lgsdir  13536  lgsne0  13539  2sqlem7  13557  neapmkvlem  13905