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

Theorem mtbird 293
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 199 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 170 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  eqneltrd  2497  neleqtrrd  2500  fvun1  5753  tz7.44-2  6624  oeeulem  6803  onomeneq  7255  cantnfp1lem2  7591  cantnflem1  7601  rankxpsuc  7762  cardaleph  7926  cfsuc  8093  cflim2  8099  addnidpi  8734  genpnnp  8838  supmul1  9929  indstr2  10510  zbtwnre  10528  xrltnsym  10686  xrlttr  10689  xralrple  10747  hashf1lem1  11659  sqrneglem  12027  rlimno1  12402  binomlem  12563  ruclem12  12795  dvdsle  12850  smu01lem  12952  rpexp  13075  oddprm  13144  pythagtriplem11  13154  pythagtriplem13  13156  pcpremul  13172  pczndvds  13193  pczndvds2  13195  pc2dvds  13207  pcadd  13213  pcmpt  13216  efgredlemc  15332  prmcyg  15458  ablfacrplem  15578  ablfac1eulem  15585  islbs2  16181  fidomndrng  16322  1stccnp  17478  fbasfip  17853  recld2  18798  metnrmlem1a  18841  xrhmeo  18924  bndth  18936  ioombl1lem4  19408  itg2seq  19587  itg2cnlem2  19607  dgrub  20106  dgrlb  20108  aaliou2  20210  taylthlem2  20243  dvlog2lem  20496  cxple2  20541  mumullem2  20916  chtub  20949  lgsval2lem  21043  lgsdir  21067  lgsne0  21070  lgsqr  21083  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem4  21089  lgsquadlem1  21091  lgsquad2  21097  m1lgs  21099  2sqlem7  21107  2sqblem  21114  usgra1v  21362  nbgranself  21399  cyclnspth  21571  eupath2lem3  21654  hmdmadj  23396  strlem1  23706  isoun  24042  ballotlem4  24709  axlowdimlem6  25790  supaddc  26137  mblfinlem3  26145  tailfb  26296  cmpfiiin  26641  fnwe2lem2  27016  frlmssuvc2  27115  dgrnznn  27208  psgnunilem1  27284  psgnunilem2  27286  stoweidlem26  27642  stoweidlem35  27651  stirlinglem5  27694  frgra2v  28103  frgrancvvdeqlem1  28133  2spotiundisj  28165  bnj1417  29116  3dimlem2  29941  3dimlem3a  29942  3dimlem3OLDN  29944  3dim2  29950  3dim3  29951  lplnnle2at  30023  lplnnlelln  30025  llncvrlpln  30040  lvolnle3at  30064  lvolnlelln  30066  lvolnlelpln  30067  4atlem3  30078  lplncvrlvol  30098  dalem30  30184  dalem35  30189  lhp2at0nle  30517  4atexlemswapqr  30545  ltrncnvel  30624  trlnle  30668  cdleme35sn3a  30941  cdleme46frvlpq  30986  cdlemeg46c  30995  cdlemeg46nlpq  30999  cdleme48gfv  31019  cdlemg7fvbwN  31089  cdlemg4d  31095  cdlemg10a  31122  cdlemg12d  31128  cdlemg27b  31178  cdlemg31d  31182  dihmeetlem6  31792  dochshpsat  31937  dochexmidlem1  31943  mapdindp  32154  lspindp5  32253
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 178
  Copyright terms: Public domain W3C validator