MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbird Structured version   Unicode version

Theorem mtbird 301
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
StepHypRef Expression
1 mtbird.min . 2  |-  ( ph  ->  -.  ch )
2 mtbird.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimpd 207 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 177 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  eqneltrd  2566  neleqtrrdOLD  2571  fvun1  5944  tz7.44-2  7091  oeeulem  7268  onomeneq  7726  supgtoreq  7946  cantnfp1lem2  8115  cantnflem1  8125  cantnfp1lem2OLD  8141  cantnflem1OLD  8148  rankxpsuc  8317  cardaleph  8487  cfsuc  8654  cflim2  8660  addnidpi  9296  genpnnp  9400  supmul1  10528  indstr2  11185  zbtwnre  11205  xrltnsym  11368  xrlttr  11371  xralrple  11429  supicclub2  11696  hashf1lem1  12507  swrdnd  12667  swrd0  12669  sqrtneglem  13111  rlimno1  13487  binomlem  13652  ruclem12  13985  dvdsle  14042  smu01lem  14146  rpexp  14272  oddprm  14350  pythagtriplem11  14360  pythagtriplem13  14362  pcpremul  14378  pczndvds  14399  pczndvds2  14401  pc2dvds  14413  pcadd  14419  pcmpt  14422  sgrp2nmndlem5  16173  pmtrdifellem4  16630  psgnunilem1  16644  psgnunilem2  16646  efgredlemc  16889  prmcyg  17022  ablfacrplem  17242  ablfac1eulem  17249  islbs2  17926  fidomndrng  18082  frlmssuvc2  18952  frlmssuvc2OLD  18954  1stccnp  20088  fbasfip  20494  recld2  21444  metnrmlem1a  21487  xrhmeo  21571  bndth  21583  ioombl1lem4  22096  itg2seq  22274  itg2cnlem2  22294  dgrub  22756  dgrlb  22758  dgrnznn  22769  aaliou2  22861  taylthlem2  22894  dvlog2lem  23158  cxple2  23203  mumullem2  23579  chtub  23612  lgsval2lem  23706  lgsdir  23730  lgsne0  23733  lgsqr  23746  lgseisenlem1  23749  lgseisenlem2  23750  lgseisenlem4  23752  lgsquadlem1  23754  lgsquad2  23760  m1lgs  23762  2sqlem7  23770  2sqblem  23777  legso  24110  mirbtwnhl  24185  axlowdimlem6  24376  usgra1v  24516  nbgranself  24560  cyclnspth  24757  eupath2lem3  25105  frgra2v  25125  frgrancvvdeqlem1  25156  2spotiundisj  25188  hmdmadj  26985  strlem1  27295  isoun  27668  archirng  27884  ballotlem4  28612  signswmnd  28689  signslema  28694  supaddc  30203  mblfinlem4  30216  tailfb  30357  cmpfiiin  30791  fnwe2lem2  31159  cvgdvgrat  31356  flltnz  31659  gtnelioc  31684  ltnelicc  31691  gtnelicc  31694  fprodn0f  31755  limciccioolb  31788  limcrecl  31796  limcicciooub  31804  limclner  31818  reclimc  31820  sinaover2ne0  31829  icccncfext  31851  jumpncnp  31862  dvmptdiv  31875  itgsincmulx  31934  stoweidlem26  31969  stoweidlem35  31978  stirlinglem5  32021  dirker2re  32035  dirkerdenne0  32036  dirkertrigeqlem3  32043  dirkertrigeq  32044  dirkercncflem1  32046  dirkercncflem2  32047  dirkercncflem4  32049  fourierdlem10  32060  fourierdlem24  32074  fourierdlem25  32075  fourierdlem42  32092  fourierdlem44  32094  fourierdlem53  32103  fourierdlem58  32108  fourierdlem62  32112  fourierdlem76  32126  fourierdlem88  32138  fourierdlem104  32154  etransclem41  32219  etransclem44  32222  usgedgnlp  32630  0nodd  32718  2nodd  32720  lindslinindsimp1  33160  bnj1417  34198  3dimlem2  35284  3dimlem3a  35285  3dimlem3OLDN  35287  3dim2  35293  3dim3  35294  lplnnle2at  35366  lplnnlelln  35368  llncvrlpln  35383  lvolnle3at  35407  lvolnlelln  35409  lvolnlelpln  35410  4atlem3  35421  lplncvrlvol  35441  dalem30  35527  dalem35  35532  lhp2at0nle  35860  4atexlemswapqr  35888  ltrncnvel  35967  trlnle  36012  cdleme35sn3a  36286  cdleme46frvlpq  36331  cdlemeg46c  36340  cdlemeg46nlpq  36344  cdleme48gfv  36364  cdlemg7fvbwN  36434  cdlemg4d  36440  cdlemg10a  36467  cdlemg12d  36473  cdlemg27b  36523  cdlemg31d  36527  dihmeetlem6  37137  dochshpsat  37282  dochexmidlem1  37288  mapdindp  37499  lspindp5  37598
  Copyright terms: Public domain W3C validator