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  2536  neleqtrrdOLD  2541  fvun1  5783  tz7.44-2  6884  oeeulem  7061  onomeneq  7521  cantnfp1lem2  7908  cantnflem1  7918  cantnfp1lem2OLD  7934  cantnflem1OLD  7941  rankxpsuc  8110  cardaleph  8280  cfsuc  8447  cflim2  8453  addnidpi  9091  genpnnp  9195  supmul1  10316  indstr2  10954  zbtwnre  10972  xrltnsym  11135  xrlttr  11138  xralrple  11196  hashf1lem1  12229  swrd0  12348  sqrneglem  12777  rlimno1  13152  binomlem  13313  ruclem12  13544  dvdsle  13599  smu01lem  13702  rpexp  13827  oddprm  13903  pythagtriplem11  13913  pythagtriplem13  13915  pcpremul  13931  pczndvds  13952  pczndvds2  13954  pc2dvds  13966  pcadd  13972  pcmpt  13975  pmtrdifellem4  16006  psgnunilem1  16020  psgnunilem2  16022  efgredlemc  16263  prmcyg  16391  ablfacrplem  16588  ablfac1eulem  16595  islbs2  17257  fidomndrng  17401  frlmssuvc2  18242  frlmssuvc2OLD  18244  1stccnp  19088  fbasfip  19463  recld2  20413  metnrmlem1a  20456  xrhmeo  20540  bndth  20552  ioombl1lem4  21064  itg2seq  21242  itg2cnlem2  21262  dgrub  21724  dgrlb  21726  aaliou2  21828  taylthlem2  21861  dvlog2lem  22119  cxple2  22164  mumullem2  22540  chtub  22573  lgsval2lem  22667  lgsdir  22691  lgsne0  22694  lgsqr  22707  lgseisenlem1  22710  lgseisenlem2  22711  lgseisenlem4  22713  lgsquadlem1  22715  lgsquad2  22721  m1lgs  22723  2sqlem7  22731  2sqblem  22738  axlowdimlem6  23215  usgra1v  23330  nbgranself  23367  cyclnspth  23539  eupath2lem3  23622  hmdmadj  25366  strlem1  25676  isoun  26019  archirng  26227  archiabllem2b  26235  ballotlem4  26903  signslema  26985  supaddc  28443  mblfinlem4  28457  tailfb  28624  cmpfiiin  29059  fnwe2lem2  29430  dgrnznn  29518  stoweidlem26  29847  stoweidlem35  29856  stirlinglem5  29899  frgra2v  30617  frgrancvvdeqlem1  30649  2spotiundisj  30681  supgtoreq  30772  lindslinindsimp1  30988  bnj1417  32128  3dimlem2  33199  3dimlem3a  33200  3dimlem3OLDN  33202  3dim2  33208  3dim3  33209  lplnnle2at  33281  lplnnlelln  33283  llncvrlpln  33298  lvolnle3at  33322  lvolnlelln  33324  lvolnlelpln  33325  4atlem3  33336  lplncvrlvol  33356  dalem30  33442  dalem35  33447  lhp2at0nle  33775  4atexlemswapqr  33803  ltrncnvel  33882  trlnle  33926  cdleme35sn3a  34199  cdleme46frvlpq  34244  cdlemeg46c  34253  cdlemeg46nlpq  34257  cdleme48gfv  34277  cdlemg7fvbwN  34347  cdlemg4d  34353  cdlemg10a  34380  cdlemg12d  34386  cdlemg27b  34436  cdlemg31d  34440  dihmeetlem6  35050  dochshpsat  35195  dochexmidlem1  35201  mapdindp  35412  lspindp5  35511
  Copyright terms: Public domain W3C validator