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

Theorem mtbird 292
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 198 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 168 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  eqneltrd  2376  neleqtrrd  2379  fvun1  5590  tz7.44-2  6420  omopth2  6582  oeeulem  6599  onomeneq  7050  cantnfp1lem2  7381  cantnflem1  7391  rankxpsuc  7552  cardaleph  7716  cfsuc  7883  cflim2  7889  addnidpi  8525  genpnnp  8629  supmul1  9719  indstr2  10296  zbtwnre  10314  xrltnsym  10471  xrlttr  10474  xralrple  10532  hashf1lem1  11393  sqrneglem  11752  rlimno1  12127  binomlem  12287  ruclem12  12519  dvdsle  12574  smu01lem  12676  rpexp  12799  oddprm  12868  pythagtriplem11  12878  pythagtriplem13  12880  pcpremul  12896  pczndvds  12917  pczndvds2  12919  pc2dvds  12931  pcadd  12937  pcmpt  12940  efgredlemc  15054  prmcyg  15180  ablfacrplem  15300  ablfac1eulem  15307  lspindp4  15890  lsppratlem3  15902  islbs2  15907  fidomndrng  16048  mplcoe1  16209  mplcoe2  16211  1stccnp  17188  fbasfip  17563  recld2  18320  metnrmlem1a  18362  xrhmeo  18444  bndth  18456  lebnumlem1  18459  ioombl1lem4  18918  itg2seq  19097  itg2cnlem2  19117  dgrub  19616  dgrlb  19618  aaliou2  19720  taylthlem2  19753  dvlog2lem  19999  cxple2  20044  mumullem2  20418  chtub  20451  lgsval2lem  20545  lgsdir  20569  lgsne0  20572  lgsqr  20585  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem4  20591  lgsquadlem1  20593  lgsquad2  20599  m1lgs  20601  2sqlem7  20609  2sqblem  20616  hmdmadj  22520  strlem1  22830  ballotlem4  23057  eupath2lem3  23903  axlowdimlem6  24575  iintlem1  25610  pdiveql  26168  tailfb  26326  cmpfiiin  26772  fnwe2lem2  27148  frlmssuvc2  27247  frlmlbs  27249  dgrnznn  27340  psgnunilem1  27416  psgnunilem2  27418  fnchoice  27700  stoweidlem23  27772  stoweidlem26  27775  stoweidlem34  27783  stoweidlem35  27784  stoweidlem59  27808  stirlinglem5  27827  usgra1v  28126  nbgranself  28149  frgra2v  28177  bnj1417  29071  3dimlem2  29648  3dimlem3a  29649  3dimlem3OLDN  29651  3dim2  29657  3dim3  29658  islln2a  29706  lplnnle2at  29730  lplnnlelln  29732  islpln2a  29737  llncvrlpln  29747  lvolnle3at  29771  lvolnlelln  29773  lvolnlelpln  29774  islvol2aN  29781  4atlem3  29785  lplncvrlvol  29805  dalem30  29891  dalem35  29896  lhp2at0nle  30224  4atexlemswapqr  30252  ltrncnvel  30331  trlnle  30375  cdleme35sn3a  30648  cdleme46frvlpq  30693  cdlemeg46c  30702  cdlemeg46nlpq  30706  cdleme48gfv  30726  cdlemg7fvbwN  30796  cdlemg4d  30802  cdlemg10a  30829  cdlemg12d  30835  cdlemg27b  30885  cdlemg31d  30889  dihmeetlem6  31499  dochshpsat  31644  dochexmidlem1  31650  mapdindp  31861  mapdindp2  31911  mapdindp4  31913  mapdh6dN  31929  lspindp5  31960  hdmap1l6d  32004
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator