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  2526  neleqtrrd  2529  fvun1  5750  tz7.44-2  6849  oeeulem  7028  onomeneq  7488  cantnfp1lem2  7875  cantnflem1  7885  cantnfp1lem2OLD  7901  cantnflem1OLD  7908  rankxpsuc  8077  cardaleph  8247  cfsuc  8414  cflim2  8420  addnidpi  9057  genpnnp  9161  supmul1  10282  indstr2  10920  zbtwnre  10938  xrltnsym  11101  xrlttr  11104  xralrple  11162  hashf1lem1  12191  swrd0  12310  sqrneglem  12739  rlimno1  13114  binomlem  13274  ruclem12  13505  dvdsle  13560  smu01lem  13663  rpexp  13788  oddprm  13864  pythagtriplem11  13874  pythagtriplem13  13876  pcpremul  13892  pczndvds  13913  pczndvds2  13915  pc2dvds  13927  pcadd  13933  pcmpt  13936  pmtrdifellem4  15964  psgnunilem1  15978  psgnunilem2  15980  efgredlemc  16221  prmcyg  16349  ablfacrplem  16539  ablfac1eulem  16546  islbs2  17156  fidomndrng  17300  frlmssuvc2  18061  frlmssuvc2OLD  18063  1stccnp  18907  fbasfip  19282  recld2  20232  metnrmlem1a  20275  xrhmeo  20359  bndth  20371  ioombl1lem4  20883  itg2seq  21061  itg2cnlem2  21081  dgrub  21586  dgrlb  21588  aaliou2  21690  taylthlem2  21723  dvlog2lem  21981  cxple2  22026  mumullem2  22402  chtub  22435  lgsval2lem  22529  lgsdir  22553  lgsne0  22556  lgsqr  22569  lgseisenlem1  22572  lgseisenlem2  22573  lgseisenlem4  22575  lgsquadlem1  22577  lgsquad2  22583  m1lgs  22585  2sqlem7  22593  2sqblem  22600  axlowdimlem6  23015  usgra1v  23130  nbgranself  23167  cyclnspth  23339  eupath2lem3  23422  hmdmadj  25166  strlem1  25476  isoun  25820  archirng  26028  archiabllem2b  26036  ballotlem4  26728  signslema  26810  supaddc  28258  mblfinlem4  28272  tailfb  28439  cmpfiiin  28875  fnwe2lem2  29246  dgrnznn  29334  stoweidlem26  29664  stoweidlem35  29673  stirlinglem5  29716  frgra2v  30434  frgrancvvdeqlem1  30466  2spotiundisj  30498  lindslinindsimp1  30697  bnj1417  31731  3dimlem2  32673  3dimlem3a  32674  3dimlem3OLDN  32676  3dim2  32682  3dim3  32683  lplnnle2at  32755  lplnnlelln  32757  llncvrlpln  32772  lvolnle3at  32796  lvolnlelln  32798  lvolnlelpln  32799  4atlem3  32810  lplncvrlvol  32830  dalem30  32916  dalem35  32921  lhp2at0nle  33249  4atexlemswapqr  33277  ltrncnvel  33356  trlnle  33400  cdleme35sn3a  33673  cdleme46frvlpq  33718  cdlemeg46c  33727  cdlemeg46nlpq  33731  cdleme48gfv  33751  cdlemg7fvbwN  33821  cdlemg4d  33827  cdlemg10a  33854  cdlemg12d  33860  cdlemg27b  33910  cdlemg31d  33914  dihmeetlem6  34524  dochshpsat  34669  dochexmidlem1  34675  mapdindp  34886  lspindp5  34985
  Copyright terms: Public domain W3C validator