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

Theorem mtbird 302
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 210 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 180 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  eqneltrd  2528  nelsn  4030  fvun1  5953  tz7.44-2  7137  oeeulem  7314  onomeneq  7772  supgtoreq  7996  inflb  8015  cantnfp1lem2  8193  cantnflem1  8203  rankxpsuc  8362  cardaleph  8528  cfsuc  8695  cflim2  8701  addnidpi  9334  genpnnp  9438  supaddc  10582  supmul1  10584  indstr2  11245  zbtwnre  11270  xrltnsym  11444  xrlttr  11447  xralrple  11506  supicclub2  11791  hashf1lem1  12623  swrdnd  12791  swrd0  12793  sqrtneglem  13331  rlimno1  13717  binomlem  13887  fprodn0f  14045  ruclem12  14293  dvdsle  14350  smu01lem  14459  rpexp  14672  oddprm  14765  pythagtriplem11  14775  pythagtriplem13  14777  pcpremul  14793  pczndvds  14814  pczndvds2  14816  pc2dvds  14828  pcadd  14834  pcmpt  14837  sgrp2nmndlem5  16663  pmtrdifellem4  17120  psgnunilem1  17134  psgnunilem2  17136  efgredlemc  17395  prmcyg  17528  ablfacrplem  17698  ablfac1eulem  17705  islbs2  18377  fidomndrng  18531  frlmssuvc2  19352  1stccnp  20476  fbasfip  20882  recld2  21831  metnrmlem1a  21874  metnrmlem1aOLD  21889  xrhmeo  21973  bndth  21985  ioombl1lem4  22513  itg2seq  22699  itg2cnlem2  22719  dgrub  23187  dgrlb  23189  dgrnznn  23200  aaliou2  23295  taylthlem2  23328  dvlog2lem  23596  cxple2  23641  mumullem2  24106  chtub  24139  lgsval2lem  24233  lgsdir  24257  lgsne0  24260  lgsqr  24273  lgseisenlem1  24276  lgseisenlem2  24277  lgseisenlem4  24279  lgsquadlem1  24281  lgsquad2  24287  m1lgs  24289  2sqlem7  24297  2sqblem  24304  legso  24643  mirbtwnhl  24724  lmiopp  24843  axlowdimlem6  24976  usgra1v  25116  nbgranself  25161  cyclnspth  25358  eupath2lem3  25706  frgra2v  25726  frgrancvvdeqlem1  25757  2spotiundisj  25789  hmdmadj  27592  strlem1  27902  isoun  28285  archirng  28513  esumrnmpt2  28898  ballotlem4  29340  signswmnd  29455  signslema  29460  bnj1417  29859  tailfb  31039  topdifinffinlem  31715  icorempt2  31719  finxpreclem6  31753  mblfinlem4  31945  3dimlem2  32994  3dimlem3a  32995  3dimlem3OLDN  32997  3dim2  33003  3dim3  33004  lplnnle2at  33076  lplnnlelln  33078  llncvrlpln  33093  lvolnle3at  33117  lvolnlelln  33119  lvolnlelpln  33120  4atlem3  33131  lplncvrlvol  33151  dalem30  33237  dalem35  33242  lhp2at0nle  33570  4atexlemswapqr  33598  ltrncnvel  33677  trlnle  33722  cdleme35sn3a  33996  cdleme46frvlpq  34041  cdlemeg46c  34050  cdlemeg46nlpq  34054  cdleme48gfv  34074  cdlemg7fvbwN  34144  cdlemg4d  34150  cdlemg10a  34177  cdlemg12d  34183  cdlemg27b  34233  cdlemg31d  34237  dihmeetlem6  34847  dochshpsat  34992  dochexmidlem1  34998  mapdindp  35209  lspindp5  35308  cmpfiiin  35509  fnwe2lem2  35880  relexpmulg  36273  relexp01min  36276  relexpxpmin  36280  cvgdvgrat  36633  flltnz  37471  gtnelioc  37537  ltnelicc  37544  gtnelicc  37547  limciccioolb  37642  limcrecl  37650  limcicciooub  37658  limclner  37673  reclimc  37675  sinaover2ne0  37684  icccncfext  37706  jumpncnp  37717  dvmptdiv  37730  itgsincmulx  37792  stoweidlem26  37827  stoweidlem35  37837  stirlinglem5  37881  dirker2re  37895  dirkerdenne0  37896  dirkertrigeqlem3  37903  dirkertrigeq  37904  dirkercncflem1  37906  dirkercncflem2  37907  dirkercncflem4  37909  fourierdlem10  37920  fourierdlem24  37934  fourierdlem25  37935  fourierdlem42  37953  fourierdlem42OLD  37954  fourierdlem44  37956  fourierdlem53  37964  fourierdlem58  37969  fourierdlem62  37973  fourierdlem76  37987  fourierdlem88  37999  fourierdlem104  38015  etransclem41  38081  etransclem44  38084  bits0eALTV  38680  oddprmALTV  38687  usgedgnlp  39371  0nodd  39459  2nodd  39461  lindslinindsimp1  39901
  Copyright terms: Public domain W3C validator