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  2389  neleqtrrd  2392  fvun1  5606  tz7.44-2  6436  omopth2  6598  oeeulem  6615  onomeneq  7066  cantnfp1lem2  7397  cantnflem1  7407  rankxpsuc  7568  cardaleph  7732  cfsuc  7899  cflim2  7905  addnidpi  8541  genpnnp  8645  supmul1  9735  indstr2  10312  zbtwnre  10330  xrltnsym  10487  xrlttr  10490  xralrple  10548  hashf1lem1  11409  sqrneglem  11768  rlimno1  12143  binomlem  12303  ruclem12  12535  dvdsle  12590  smu01lem  12692  rpexp  12815  oddprm  12884  pythagtriplem11  12894  pythagtriplem13  12896  pcpremul  12912  pczndvds  12933  pczndvds2  12935  pc2dvds  12947  pcadd  12953  pcmpt  12956  efgredlemc  15070  prmcyg  15196  ablfacrplem  15316  ablfac1eulem  15323  lspindp4  15906  lsppratlem3  15918  islbs2  15923  fidomndrng  16064  mplcoe1  16225  mplcoe2  16227  1stccnp  17204  fbasfip  17579  recld2  18336  metnrmlem1a  18378  xrhmeo  18460  bndth  18472  lebnumlem1  18475  ioombl1lem4  18934  itg2seq  19113  itg2cnlem2  19133  dgrub  19632  dgrlb  19634  aaliou2  19736  taylthlem2  19769  dvlog2lem  20015  cxple2  20060  mumullem2  20434  chtub  20467  lgsval2lem  20561  lgsdir  20585  lgsne0  20588  lgsqr  20601  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem4  20607  lgsquadlem1  20609  lgsquad2  20615  m1lgs  20617  2sqlem7  20625  2sqblem  20632  hmdmadj  22536  strlem1  22846  ballotlem4  23073  eupath2lem3  23918  axlowdimlem6  24647  supaddc  24995  iintlem1  25713  pdiveql  26271  tailfb  26429  cmpfiiin  26875  fnwe2lem2  27251  frlmssuvc2  27350  frlmlbs  27352  dgrnznn  27443  psgnunilem1  27519  psgnunilem2  27521  fnchoice  27803  stoweidlem23  27875  stoweidlem26  27878  stoweidlem34  27886  stoweidlem35  27887  stoweidlem59  27911  stirlinglem5  27930  usgra1v  28260  nbgranself  28283  cyclnspth  28376  frgra2v  28423  bnj1417  29387  3dimlem2  30270  3dimlem3a  30271  3dimlem3OLDN  30273  3dim2  30279  3dim3  30280  islln2a  30328  lplnnle2at  30352  lplnnlelln  30354  islpln2a  30359  llncvrlpln  30369  lvolnle3at  30393  lvolnlelln  30395  lvolnlelpln  30396  islvol2aN  30403  4atlem3  30407  lplncvrlvol  30427  dalem30  30513  dalem35  30518  lhp2at0nle  30846  4atexlemswapqr  30874  ltrncnvel  30953  trlnle  30997  cdleme35sn3a  31270  cdleme46frvlpq  31315  cdlemeg46c  31324  cdlemeg46nlpq  31328  cdleme48gfv  31348  cdlemg7fvbwN  31418  cdlemg4d  31424  cdlemg10a  31451  cdlemg12d  31457  cdlemg27b  31507  cdlemg31d  31511  dihmeetlem6  32121  dochshpsat  32266  dochexmidlem1  32272  mapdindp  32483  mapdindp2  32533  mapdindp4  32535  mapdh6dN  32551  lspindp5  32582  hdmap1l6d  32626
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