Theorem mtbird 680

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 669	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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2327  neleqtrrd  2330  eqnbrtrd  4111  fidifsnen  7100  php5fin  7114  tridc  7132  fimax2gtrilemstep  7133  en2eqpr  7142  inflbti  7266  omp1eomlem  7336  difinfsnlem  7341  addnidpig  7599  nqnq0pi  7701  ltpopr  7858  cauappcvgprlemladdru  7919  caucvgprlemladdrl  7941  caucvgprprlemnkltj  7952  caucvgprprlemnkeqj  7953  caucvgprprlemaddq  7971  ltposr  8026  axpre-suploclemres  8164  axltirr  8288  reapirr  8799  apirr  8827  indstr2  9887  xrltnsym  10072  xrlttr  10074  xrltso  10075  xltadd1  10155  xposdif  10161  xleaddadd  10166  lbioog  10192  ubioog  10193  fzn  10322  xqltnle  10573  flqltnz  10593  iseqf1olemnab  10809  iseqf1olemqk  10815  exp3val  10849  fihashelne0d  11105  zfz1isolemiso  11149  swrdnd  11289  swrd0g  11290  xrmaxltsup  11881  binomlem  12107  dvdsle  12468  2tp1odd  12508  divalglemeuneg  12547  bits0e  12573  bezoutlemle  12642  rpexp  12788  oddpwdclemxy  12804  oddpwdclemndvds  12806  sqpweven  12810  2sqpwodd  12811  oddprm  12895  pythagtriplem11  12910  pythagtriplem13  12912  pcpremul  12929  pczndvds2  12954  pc2dvds  12966  pcmpt  12979  ctinfom  13112  aprirr  14362  ivthinc  15437  logbgcd1irraplemexp  15762  lgsval2lem  15812  lgsdir  15837  lgsne0  15840  gausslemma2dlem1f1o  15862  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem4  15875  lgsquadlem1  15879  lgsquad2  15885  m1lgs  15887  2sqlem7  15923  1loopgrvd0fi  16230  qdiff  16764  neapmkvlem  16783