MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbird 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
mtbird.maj
Assertion
Ref Expression
mtbird

Proof of Theorem mtbird
StepHypRef Expression
1 mtbird.min . 2
2 mtbird.maj . . 3
32biimpd 207 . 2
41, 3mtod 177 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  eqneltrd  2566  neleqtrrdOLD  2571  fvun1  5944  tz7.44-2  7092  oeeulem  7269  onomeneq  7727  supgtoreq  7949  cantnfp1lem2  8119  cantnflem1  8129  cantnfp1lem2OLD  8145  cantnflem1OLD  8152  rankxpsuc  8321  cardaleph  8491  cfsuc  8658  cflim2  8664  addnidpi  9300  genpnnp  9404  supmul1  10533  indstr2  11189  zbtwnre  11209  xrltnsym  11372  xrlttr  11375  xralrple  11433  supicclub2  11700  hashf1lem1  12504  swrd0  12658  sqrtneglem  13100  rlimno1  13476  binomlem  13641  ruclem12  13974  dvdsle  14031  smu01lem  14135  rpexp  14261  oddprm  14339  pythagtriplem11  14349  pythagtriplem13  14351  pcpremul  14367  pczndvds  14388  pczndvds2  14390  pc2dvds  14402  pcadd  14408  pcmpt  14411  sgrp2nmndlem5  16047  pmtrdifellem4  16504  psgnunilem1  16518  psgnunilem2  16520  efgredlemc  16763  prmcyg  16896  ablfacrplem  17116  ablfac1eulem  17123  islbs2  17800  fidomndrng  17956  frlmssuvc2  18826  frlmssuvc2OLD  18828  1stccnp  19963  fbasfip  20369  recld2  21319  metnrmlem1a  21362  xrhmeo  21446  bndth  21458  ioombl1lem4  21971  itg2seq  22149  itg2cnlem2  22169  dgrub  22631  dgrlb  22633  dgrnznn  22644  aaliou2  22736  taylthlem2  22769  dvlog2lem  23033  cxple2  23078  mumullem2  23454  chtub  23487  lgsval2lem  23581  lgsdir  23605  lgsne0  23608  lgsqr  23621  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem4  23627  lgsquadlem1  23629  lgsquad2  23635  m1lgs  23637  2sqlem7  23645  2sqblem  23652  legso  23985  mirbtwnhl  24060  axlowdimlem6  24250  usgra1v  24390  nbgranself  24434  cyclnspth  24631  eupath2lem3  24979  frgra2v  24999  frgrancvvdeqlem1  25030  2spotiundisj  25062  hmdmadj  26859  strlem1  27169  isoun  27520  archirng  27732  ballotlem4  28437  signswmnd  28514  signslema  28519  supaddc  30041  mblfinlem4  30054  tailfb  30195  cmpfiiin  30629  fnwe2lem2  30997  cvgdvgrat  31194  flltnz  31498  gtnelioc  31523  ltnelicc  31530  gtnelicc  31533  fprodn0f  31594  limciccioolb  31627  limcrecl  31635  limcicciooub  31643  limclner  31657  reclimc  31659  sinaover2ne0  31668  icccncfext  31690  jumpncnp  31701  dvmptdiv  31714  itgsincmulx  31773  stoweidlem26  31808  stoweidlem35  31817  stirlinglem5  31860  dirker2re  31874  dirkerdenne0  31875  dirkertrigeqlem3  31882  dirkertrigeq  31883  dirkercncflem1  31885  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem10  31899  fourierdlem24  31913  fourierdlem25  31914  fourierdlem42  31931  fourierdlem44  31933  fourierdlem53  31942  fourierdlem58  31947  fourierdlem62  31951  fourierdlem76  31965  fourierdlem88  31977  fourierdlem104  31993  etransclem41  32058  etransclem44  32061  usgedgnlp  32410  0nodd  32498  2nodd  32500  lindslinindsimp1  33058  bnj1417  34097  3dimlem2  35183  3dimlem3a  35184  3dimlem3OLDN  35186  3dim2  35192  3dim3  35193  lplnnle2at  35265  lplnnlelln  35267  llncvrlpln  35282  lvolnle3at  35306  lvolnlelln  35308  lvolnlelpln  35309  4atlem3  35320  lplncvrlvol  35340  dalem30  35426  dalem35  35431  lhp2at0nle  35759  4atexlemswapqr  35787  ltrncnvel  35866  trlnle  35911  cdleme35sn3a  36185  cdleme46frvlpq  36230  cdlemeg46c  36239  cdlemeg46nlpq  36243  cdleme48gfv  36263  cdlemg7fvbwN  36333  cdlemg4d  36339  cdlemg10a  36366  cdlemg12d  36372  cdlemg27b  36422  cdlemg31d  36426  dihmeetlem6  37036  dochshpsat  37181  dochexmidlem1  37187  mapdindp  37398  lspindp5  37497
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
  Copyright terms: Public domain W3C validator