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  4148  fidifsnen  7172  php5fin  7186  tridc  7204  fimax2gtrilemstep  7205  en2eqpr  7214  inflbti  7365  omp1eomlem  7435  difinfsnlem  7440  addnidpig  7704  nqnq0pi  7806  ltpopr  7963  cauappcvgprlemladdru  8024  caucvgprlemladdrl  8046  caucvgprprlemnkltj  8057  caucvgprprlemnkeqj  8058  caucvgprprlemaddq  8076  ltposr  8131  axpre-suploclemres  8269  axltirr  8393  reapirr  8908  apirr  8936  indstr2  10019  xrltnsym  10206  xrlttr  10208  xrltso  10209  xltadd1  10289  xposdif  10295  xleaddadd  10300  lbioog  10326  ubioog  10327  fzn  10457  xqltnle  10713  flqltnz  10737  iseqf1olemnab  10953  iseqf1olemqk  10959  exp3val  10993  fihashelne0d  11252  hashf1lem1  11301  zfz1isolemiso  11307  swrdnd  11447  swrd0g  11448  xrmaxltsup  12043  binomlem  12269  dvdsle  12630  2tp1odd  12670  divalglemeuneg  12709  bits0e  12735  bezoutlemle  12804  rpexp  12951  nnmaxpwlemxy  12967  sqpweven  12974  2sqpwodd  12975  oddprm  13061  pythagtriplem11  13076  pythagtriplem13  13078  pcpremul  13095  pczndvds2  13120  pc2dvds  13132  pcmpt  13145  ballotfilem4  13293  ctinfom  13371  aprirr  14679  ivthinc  15835  logbgcd1irraplemexp  16165  birthdaylem3  16188  chtqub  16257  lgsval2lem  16295  lgsdir  16320  lgsne0  16323  gausslemma2dlem1f1o  16345  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem4  16358  lgsquadlem1  16362  lgsquad2  16368  m1lgs  16370  2sqlem7  16406  1loopgrvd0fi  16713  rirrdisj  17251  qdiff  17265  neapmkvlem  17284