Theorem mtbird 677

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2325  neleqtrrd  2328  eqnbrtrd  4101  fidifsnen  7040  php5fin  7052  tridc  7070  fimax2gtrilemstep  7071  en2eqpr  7080  inflbti  7202  omp1eomlem  7272  difinfsnlem  7277  addnidpig  7534  nqnq0pi  7636  ltpopr  7793  cauappcvgprlemladdru  7854  caucvgprlemladdrl  7876  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemaddq  7906  ltposr  7961  axpre-suploclemres  8099  axltirr  8224  reapirr  8735  apirr  8763  indstr2  9816  xrltnsym  10001  xrlttr  10003  xrltso  10004  xltadd1  10084  xposdif  10090  xleaddadd  10095  lbioog  10121  ubioog  10122  fzn  10250  xqltnle  10499  flqltnz  10519  iseqf1olemnab  10735  iseqf1olemqk  10741  exp3val  10775  fihashelne0d  11031  zfz1isolemiso  11074  swrdnd  11206  swrd0g  11207  xrmaxltsup  11784  binomlem  12009  dvdsle  12370  2tp1odd  12410  divalglemeuneg  12449  bits0e  12475  bezoutlemle  12544  rpexp  12690  oddpwdclemxy  12706  oddpwdclemndvds  12708  sqpweven  12712  2sqpwodd  12713  oddprm  12797  pythagtriplem11  12812  pythagtriplem13  12814  pcpremul  12831  pczndvds2  12856  pc2dvds  12868  pcmpt  12881  ctinfom  13014  aprirr  14262  ivthinc  15332  logbgcd1irraplemexp  15657  lgsval2lem  15704  lgsdir  15729  lgsne0  15732  gausslemma2dlem1f1o  15754  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem4  15767  lgsquadlem1  15771  lgsquad2  15777  m1lgs  15779  2sqlem7  15815  neapmkvlem  16495