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 )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  eqneltrd  2334  neleqtrrd  2337  eqnbrtrd  4149  fidifsnen  7176  php5fin  7190  tridc  7208  fimax2gtrilemstep  7209  en2eqpr  7218  inflbti  7370  omp1eomlem  7440  difinfsnlem  7445  addnidpig  7709  nqnq0pi  7811  ltpopr  7968  cauappcvgprlemladdru  8029  caucvgprlemladdrl  8051  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  caucvgprprlemaddq  8081  ltposr  8136  axpre-suploclemres  8274  axltirr  8398  reapirr  8913  apirr  8941  indstr2  10025  xrltnsym  10212  xrlttr  10214  xrltso  10215  xltadd1  10295  xposdif  10301  xleaddadd  10306  lbioog  10332  ubioog  10333  fzn  10463  xqltnle  10719  flqltnz  10743  iseqf1olemnab  10959  iseqf1olemqk  10965  exp3val  10999  fihashelne0d  11258  hashf1lem1  11307  zfz1isolemiso  11313  swrdnd  11453  swrd0g  11454  xrmaxltsup  12049  binomlem  12275  dvdsle  12636  2tp1odd  12676  divalglemeuneg  12715  bits0e  12741  bezoutlemle  12810  rpexp  12957  nnmaxpwlemxy  12973  sqpweven  12980  2sqpwodd  12981  oddprm  13067  pythagtriplem11  13082  pythagtriplem13  13084  pcpremul  13101  pczndvds2  13126  pc2dvds  13138  pcmpt  13151  ballotfilem4  13299  ctinfom  13377  aprirr  14704  ivthinc  15869  logbgcd1irraplemexp  16204  birthdaylem3  16227  chtqub  16296  lgsval2lem  16334  lgsdir  16359  lgsne0  16362  gausslemma2dlem1f1o  16384  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem4  16397  lgsquadlem1  16401  lgsquad2  16407  m1lgs  16409  2sqlem7  16445  1loopgrvd0fi  16752  rirrdisj  17291  qdiff  17305  neapmkvlem  17324