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  4104  fidifsnen  7052  php5fin  7064  tridc  7082  fimax2gtrilemstep  7083  en2eqpr  7092  inflbti  7214  omp1eomlem  7284  difinfsnlem  7289  addnidpig  7546  nqnq0pi  7648  ltpopr  7805  cauappcvgprlemladdru  7866  caucvgprlemladdrl  7888  caucvgprprlemnkltj  7899  caucvgprprlemnkeqj  7900  caucvgprprlemaddq  7918  ltposr  7973  axpre-suploclemres  8111  axltirr  8236  reapirr  8747  apirr  8775  indstr2  9833  xrltnsym  10018  xrlttr  10020  xrltso  10021  xltadd1  10101  xposdif  10107  xleaddadd  10112  lbioog  10138  ubioog  10139  fzn  10267  xqltnle  10517  flqltnz  10537  iseqf1olemnab  10753  iseqf1olemqk  10759  exp3val  10793  fihashelne0d  11049  zfz1isolemiso  11093  swrdnd  11230  swrd0g  11231  xrmaxltsup  11809  binomlem  12034  dvdsle  12395  2tp1odd  12435  divalglemeuneg  12474  bits0e  12500  bezoutlemle  12569  rpexp  12715  oddpwdclemxy  12731  oddpwdclemndvds  12733  sqpweven  12737  2sqpwodd  12738  oddprm  12822  pythagtriplem11  12837  pythagtriplem13  12839  pcpremul  12856  pczndvds2  12881  pc2dvds  12893  pcmpt  12906  ctinfom  13039  aprirr  14287  ivthinc  15357  logbgcd1irraplemexp  15682  lgsval2lem  15729  lgsdir  15754  lgsne0  15757  gausslemma2dlem1f1o  15779  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem4  15792  lgsquadlem1  15796  lgsquad2  15802  m1lgs  15804  2sqlem7  15840  1loopgrvd0fi  16112  neapmkvlem  16607