Theorem mtbird 684

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 673	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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2334  neleqtrrd  2337  eqnbrtrd  4143  fidifsnen  7162  php5fin  7176  tridc  7194  fimax2gtrilemstep  7195  en2eqpr  7204  inflbti  7354  omp1eomlem  7424  difinfsnlem  7429  addnidpig  7693  nqnq0pi  7795  ltpopr  7952  cauappcvgprlemladdru  8013  caucvgprlemladdrl  8035  caucvgprprlemnkltj  8046  caucvgprprlemnkeqj  8047  caucvgprprlemaddq  8065  ltposr  8120  axpre-suploclemres  8258  axltirr  8382  reapirr  8895  apirr  8923  indstr2  9988  xrltnsym  10174  xrlttr  10176  xrltso  10177  xltadd1  10257  xposdif  10263  xleaddadd  10268  lbioog  10294  ubioog  10295  fzn  10425  xqltnle  10680  flqltnz  10700  iseqf1olemnab  10916  iseqf1olemqk  10922  exp3val  10956  fihashelne0d  11214  hashf1lem1  11263  zfz1isolemiso  11269  swrdnd  11409  swrd0g  11410  xrmaxltsup  12002  binomlem  12228  dvdsle  12589  2tp1odd  12629  divalglemeuneg  12668  bits0e  12694  bezoutlemle  12763  rpexp  12909  oddpwdclemxy  12925  oddpwdclemndvds  12927  sqpweven  12931  2sqpwodd  12932  oddprm  13016  pythagtriplem11  13031  pythagtriplem13  13033  pcpremul  13050  pczndvds2  13075  pc2dvds  13087  pcmpt  13100  ballotfilem4  13219  ctinfom  13297  aprirr  14568  ivthinc  15667  logbgcd1irraplemexp  15993  lgsval2lem  16043  lgsdir  16068  lgsne0  16071  gausslemma2dlem1f1o  16093  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem4  16106  lgsquadlem1  16110  lgsquad2  16116  m1lgs  16118  2sqlem7  16154  1loopgrvd0fi  16461  qdiff  17003  neapmkvlem  17022