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  4100  fidifsnen  7028  php5fin  7040  tridc  7057  fimax2gtrilemstep  7058  en2eqpr  7065  inflbti  7187  omp1eomlem  7257  difinfsnlem  7262  addnidpig  7519  nqnq0pi  7621  ltpopr  7778  cauappcvgprlemladdru  7839  caucvgprlemladdrl  7861  caucvgprprlemnkltj  7872  caucvgprprlemnkeqj  7873  caucvgprprlemaddq  7891  ltposr  7946  axpre-suploclemres  8084  axltirr  8209  reapirr  8720  apirr  8748  indstr2  9800  xrltnsym  9985  xrlttr  9987  xrltso  9988  xltadd1  10068  xposdif  10074  xleaddadd  10079  lbioog  10105  ubioog  10106  fzn  10234  xqltnle  10482  flqltnz  10502  iseqf1olemnab  10718  iseqf1olemqk  10724  exp3val  10758  fihashelne0d  11014  zfz1isolemiso  11056  swrdnd  11186  swrd0g  11187  xrmaxltsup  11764  binomlem  11989  dvdsle  12350  2tp1odd  12390  divalglemeuneg  12429  bits0e  12455  bezoutlemle  12524  rpexp  12670  oddpwdclemxy  12686  oddpwdclemndvds  12688  sqpweven  12692  2sqpwodd  12693  oddprm  12777  pythagtriplem11  12792  pythagtriplem13  12794  pcpremul  12811  pczndvds2  12836  pc2dvds  12848  pcmpt  12861  ctinfom  12994  aprirr  14241  ivthinc  15311  logbgcd1irraplemexp  15636  lgsval2lem  15683  lgsdir  15708  lgsne0  15711  gausslemma2dlem1f1o  15733  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem4  15746  lgsquadlem1  15750  lgsquad2  15756  m1lgs  15758  2sqlem7  15794  neapmkvlem  16394