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  2330  neleqtrrd  2333  eqnbrtrd  4132  fidifsnen  7138  php5fin  7152  tridc  7170  fimax2gtrilemstep  7171  en2eqpr  7180  inflbti  7328  omp1eomlem  7398  difinfsnlem  7403  addnidpig  7667  nqnq0pi  7769  ltpopr  7926  cauappcvgprlemladdru  7987  caucvgprlemladdrl  8009  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemaddq  8039  ltposr  8094  axpre-suploclemres  8232  axltirr  8356  reapirr  8868  apirr  8896  indstr2  9959  xrltnsym  10145  xrlttr  10147  xrltso  10148  xltadd1  10228  xposdif  10234  xleaddadd  10239  lbioog  10265  ubioog  10266  fzn  10396  xqltnle  10651  flqltnz  10671  iseqf1olemnab  10887  iseqf1olemqk  10893  exp3val  10927  fihashelne0d  11185  zfz1isolemiso  11236  swrdnd  11376  swrd0g  11377  xrmaxltsup  11968  binomlem  12194  dvdsle  12555  2tp1odd  12595  divalglemeuneg  12634  bits0e  12660  bezoutlemle  12729  rpexp  12875  oddpwdclemxy  12891  oddpwdclemndvds  12893  sqpweven  12897  2sqpwodd  12898  oddprm  12982  pythagtriplem11  12997  pythagtriplem13  12999  pcpremul  13016  pczndvds2  13041  pc2dvds  13053  pcmpt  13066  ballotfilem4  13185  ctinfom  13263  aprirr  14533  ivthinc  15634  logbgcd1irraplemexp  15959  lgsval2lem  16009  lgsdir  16034  lgsne0  16037  gausslemma2dlem1f1o  16059  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem4  16072  lgsquadlem1  16076  lgsquad2  16082  m1lgs  16084  2sqlem7  16120  1loopgrvd0fi  16427  qdiff  16959  neapmkvlem  16979