MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbird Structured version   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  2528  neleqtrrd  2531  fvun1  5786  tz7.44-2  6657  oeeulem  6836  onomeneq  7288  cantnfp1lem2  7627  cantnflem1  7637  rankxpsuc  7798  cardaleph  7962  cfsuc  8129  cflim2  8135  addnidpi  8770  genpnnp  8874  supmul1  9965  indstr2  10546  zbtwnre  10564  xrltnsym  10722  xrlttr  10725  xralrple  10783  hashf1lem1  11696  sqrneglem  12064  rlimno1  12439  binomlem  12600  ruclem12  12832  dvdsle  12887  smu01lem  12989  rpexp  13112  oddprm  13181  pythagtriplem11  13191  pythagtriplem13  13193  pcpremul  13209  pczndvds  13230  pczndvds2  13232  pc2dvds  13244  pcadd  13250  pcmpt  13253  efgredlemc  15369  prmcyg  15495  ablfacrplem  15615  ablfac1eulem  15622  islbs2  16218  fidomndrng  16359  1stccnp  17517  fbasfip  17892  recld2  18837  metnrmlem1a  18880  xrhmeo  18963  bndth  18975  ioombl1lem4  19447  itg2seq  19626  itg2cnlem2  19646  dgrub  20145  dgrlb  20147  aaliou2  20249  taylthlem2  20282  dvlog2lem  20535  cxple2  20580  mumullem2  20955  chtub  20988  lgsval2lem  21082  lgsdir  21106  lgsne0  21109  lgsqr  21122  lgseisenlem1  21125  lgseisenlem2  21126  lgseisenlem4  21128  lgsquadlem1  21130  lgsquad2  21136  m1lgs  21138  2sqlem7  21146  2sqblem  21153  usgra1v  21401  nbgranself  21438  cyclnspth  21610  eupath2lem3  21693  hmdmadj  23435  strlem1  23745  isoun  24081  ballotlem4  24748  axlowdimlem6  25878  supaddc  26228  mblfinlem3  26236  tailfb  26397  cmpfiiin  26742  fnwe2lem2  27117  frlmssuvc2  27215  dgrnznn  27308  psgnunilem1  27384  psgnunilem2  27386  stoweidlem26  27742  stoweidlem35  27751  stirlinglem5  27794  frgra2v  28326  frgrancvvdeqlem1  28356  2spotiundisj  28388  bnj1417  29347  3dimlem2  30193  3dimlem3a  30194  3dimlem3OLDN  30196  3dim2  30202  3dim3  30203  lplnnle2at  30275  lplnnlelln  30277  llncvrlpln  30292  lvolnle3at  30316  lvolnlelln  30318  lvolnlelpln  30319  4atlem3  30330  lplncvrlvol  30350  dalem30  30436  dalem35  30441  lhp2at0nle  30769  4atexlemswapqr  30797  ltrncnvel  30876  trlnle  30920  cdleme35sn3a  31193  cdleme46frvlpq  31238  cdlemeg46c  31247  cdlemeg46nlpq  31251  cdleme48gfv  31271  cdlemg7fvbwN  31341  cdlemg4d  31347  cdlemg10a  31374  cdlemg12d  31380  cdlemg27b  31430  cdlemg31d  31434  dihmeetlem6  32044  dochshpsat  32189  dochexmidlem1  32195  mapdindp  32406  lspindp5  32505
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