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

Theorem mtbird 307
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 212 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 182 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  eqneltrd  2559  nelsn  4012  fvun1  5964  tz7.44-2  7156  oeeulem  7333  onomeneq  7793  supgtoreq  8017  inflb  8036  cantnfp1lem2  8215  cantnflem1  8225  rankxpsuc  8384  cardaleph  8551  cfsuc  8718  cflim2  8724  addnidpi  9357  genpnnp  9461  supaddc  10607  supmul1  10609  indstr2  11271  zbtwnre  11296  xrltnsym  11470  xrlttr  11473  xralrple  11532  supicclub2  11818  hashf1lem1  12657  swrdnd  12831  swrd0  12833  sqrtneglem  13385  rlimno1  13772  binomlem  13942  fprodn0f  14100  ruclem12  14348  dvdsle  14405  smu01lem  14514  rpexp  14727  oddprm  14820  pythagtriplem11  14830  pythagtriplem13  14832  pcpremul  14848  pczndvds  14869  pczndvds2  14871  pc2dvds  14883  pcadd  14889  pcmpt  14892  sgrp2nmndlem5  16718  pmtrdifellem4  17175  psgnunilem1  17189  psgnunilem2  17191  efgredlemc  17450  prmcyg  17583  ablfacrplem  17753  ablfac1eulem  17760  islbs2  18432  fidomndrng  18586  frlmssuvc2  19408  1stccnp  20532  fbasfip  20938  recld2  21887  metnrmlem1a  21930  metnrmlem1aOLD  21945  xrhmeo  22029  bndth  22041  ioombl1lem4  22570  itg2seq  22756  itg2cnlem2  22776  dgrub  23244  dgrlb  23246  dgrnznn  23257  aaliou2  23352  taylthlem2  23385  dvlog2lem  23653  cxple2  23698  mumullem2  24163  chtub  24196  lgsval2lem  24290  lgsdir  24314  lgsne0  24317  lgsqr  24330  lgseisenlem1  24333  lgseisenlem2  24334  lgseisenlem4  24336  lgsquadlem1  24338  lgsquad2  24344  m1lgs  24346  2sqlem7  24354  2sqblem  24361  legso  24700  mirbtwnhl  24781  lmiopp  24900  axlowdimlem6  25033  usgra1v  25173  nbgranself  25218  cyclnspth  25415  eupath2lem3  25763  frgra2v  25783  frgrancvvdeqlem1  25814  2spotiundisj  25846  hmdmadj  27649  strlem1  27959  isoun  28334  archirng  28556  esumrnmpt2  28940  ballotlem4  29381  signswmnd  29496  signslema  29501  bnj1417  29900  tailfb  31083  topdifinffinlem  31796  icorempt2  31800  finxpreclem6  31834  mblfinlem4  32026  3dimlem2  33070  3dimlem3a  33071  3dimlem3OLDN  33073  3dim2  33079  3dim3  33080  lplnnle2at  33152  lplnnlelln  33154  llncvrlpln  33169  lvolnle3at  33193  lvolnlelln  33195  lvolnlelpln  33196  4atlem3  33207  lplncvrlvol  33227  dalem30  33313  dalem35  33318  lhp2at0nle  33646  4atexlemswapqr  33674  ltrncnvel  33753  trlnle  33798  cdleme35sn3a  34072  cdleme46frvlpq  34117  cdlemeg46c  34126  cdlemeg46nlpq  34130  cdleme48gfv  34150  cdlemg7fvbwN  34220  cdlemg4d  34226  cdlemg10a  34253  cdlemg12d  34259  cdlemg27b  34309  cdlemg31d  34313  dihmeetlem6  34923  dochshpsat  35068  dochexmidlem1  35074  mapdindp  35285  lspindp5  35384  cmpfiiin  35585  fnwe2lem2  35955  relexpmulg  36348  relexp01min  36351  relexpxpmin  36355  cvgdvgrat  36707  eqnbrtrd  37461  nelrnmpt  37473  difmap  37543  flltnz  37591  gtnelioc  37672  ltnelicc  37679  gtnelicc  37682  lenelioc  37723  xrgtnelicc  37725  limciccioolb  37787  limcrecl  37795  limcicciooub  37803  limclner  37818  reclimc  37820  sinaover2ne0  37829  icccncfext  37851  jumpncnp  37862  dvmptdiv  37875  itgsincmulx  37937  stoweidlem26  37987  stoweidlem35  37997  stirlinglem5  38041  dirker2re  38055  dirkerdenne0  38056  dirkertrigeqlem3  38063  dirkertrigeq  38064  dirkercncflem1  38066  dirkercncflem2  38067  dirkercncflem4  38069  fourierdlem10  38080  fourierdlem24  38094  fourierdlem25  38095  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem44  38116  fourierdlem53  38124  fourierdlem58  38129  fourierdlem62  38133  fourierdlem76  38147  fourierdlem88  38159  fourierdlem104  38175  etransclem41  38241  etransclem44  38244  hoiqssbllem3  38553  bits0eALTV  38944  oddprmALTV  38951  usgedgnlp  40091  0nodd  40179  2nodd  40181  lindslinindsimp1  40619
  Copyright terms: Public domain W3C validator