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

Theorem mtbird 326
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 230 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 199 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207
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 208
This theorem is referenced by:  eqneltrd  2929  eqnbrtrd  5075  nsuceq0  6264  fvun1  6747  tz7.44-2  8032  oeeulem  8216  onomeneq  8696  supgtoreq  8922  inflb  8941  cantnfp1lem2  9130  cantnflem1  9140  rankxpsuc  9299  cardaleph  9503  cfsuc  9667  cflim2  9673  addnidpi  10311  genpnnp  10415  supaddc  11596  supmul1  11598  nnneneg  11660  indstr2  12315  zbtwnre  12334  xrltnsym  12518  xrlttr  12521  xralrple  12586  supicclub2  12877  flltnz  13169  hashelne0d  13717  hashf1lem1  13801  swrdnd  14004  swrd0  14008  sqrtneglem  14614  rlimno1  14998  binomlem  15172  fprodn0f  15333  ruclem12  15582  dvdsle  15648  2tp1odd  15689  smu01lem  15822  rpexp  16052  oddprm  16135  pythagtriplem11  16150  pythagtriplem13  16152  pcpremul  16168  pczndvds2  16191  pc2dvds  16203  pcmpt  16216  sgrp2nmndlem5  18032  pmtrdifellem4  18536  psgnunilem1  18550  psgnunilem2  18552  efgredlemc  18800  prmcyg  18943  ablfacrplem  19116  ablfac1eulem  19123  ablsimpgfindlem1  19158  islbs2  19855  fidomndrng  20008  frlmssuvc2  20867  1stccnp  21998  fbasfip  22404  metnrmlem1a  23393  xrhmeo  23477  bndth  23489  ioombl1lem4  24089  itg2seq  24270  dvmptdiv  24498  dgrlb  24753  dgrnznn  24764  aaliou2  24856  taylthlem2  24889  cos02pilt1  25038  dvlog2lem  25162  cxple2  25207  mumullem2  25684  chtub  25715  lgsval2lem  25810  lgsdir  25835  lgsne0  25838  lgsqr  25854  lgseisenlem1  25878  lgseisenlem2  25879  lgseisenlem4  25881  lgsquadlem1  25883  lgsquad2  25889  m1lgs  25891  2sqlem7  25927  2sqblem  25934  legso  26312  lmiopp  26515  axlowdimlem6  26660  elntg2  26698  1loopgrvd0  27213  1egrvtxdg0  27220  nfrgr2v  27978  hmdmadj  29644  strlem1  29954  isoun  30363  archirng  30744  esumrnmpt2  31226  ballotlem4  31655  signswmnd  31726  signslema  31731  bnj1417  32210  satf0n0  32522  fmlaomn0  32534  prv1n  32575  nosupbnd1lem1  33105  nosupbnd2  33113  tailfb  33622  unblimceq0  33743  unbdqndv2lem2  33746  topdifinffinlem  34510  icorempo  34514  finxpreclem6  34559  lindsadd  34766  mblfinlem4  34813  3dimlem2  36475  3dimlem3a  36476  3dimlem3OLDN  36478  3dim2  36484  3dim3  36485  lplnnle2at  36557  lplnnlelln  36559  llncvrlpln  36574  lvolnle3at  36598  lvolnlelln  36600  lvolnlelpln  36601  4atlem3  36612  lplncvrlvol  36632  dalem30  36718  dalem35  36723  lhp2at0nle  37051  4atexlemswapqr  37079  ltrncnvel  37158  trlnle  37202  cdleme35sn3a  37475  cdleme46frvlpq  37520  cdlemeg46c  37529  cdlemeg46nlpq  37533  cdleme48gfv  37553  cdlemg7fvbwN  37623  cdlemg4d  37629  cdlemg10a  37656  cdlemg12d  37662  cdlemg27b  37712  cdlemg31d  37716  dihmeetlem6  38325  dochshpsat  38470  dochexmidlem1  38476  mapdindp  38687  lspindp5  38786  xppss12  38993  oexpreposd  39057  dffltz  39149  cmpfiiin  39172  fnwe2lem2  39529  relexpmulg  39933  relexp01min  39936  relexpxpmin  39940  cvgdvgrat  40522  nelrnmpt  41225  difmap  41346  rnmptn0  41360  gtnelioc  41641  ltnelicc  41648  gtnelicc  41651  lenelioc  41688  xrgtnelicc  41690  limciccioolb  41778  limcrecl  41786  limcicciooub  41794  limclner  41808  reclimc  41810  sinaover2ne0  42025  icccncfext  42046  jumpncnp  42057  itgsincmulx  42135  stoweidlem26  42188  stoweidlem35  42197  stirlinglem5  42240  dirker2re  42254  dirkerdenne0  42255  dirkertrigeqlem3  42262  dirkertrigeq  42263  dirkercncflem1  42265  dirkercncflem2  42266  dirkercncflem4  42268  fourierdlem10  42279  fourierdlem24  42293  fourierdlem25  42294  fourierdlem42  42311  fourierdlem44  42313  fourierdlem53  42321  fourierdlem58  42326  fourierdlem62  42330  fourierdlem76  42344  fourierdlem88  42356  fourierdlem104  42372  etransclem41  42437  etransclem44  42440  hoiqssbllem3  42783  ichnreuop  43511  fmtnoinf  43575  lighneallem3  43649  lighneallem4  43652  bits0eALTV  43722  oddprmALTV  43729  0nodd  43954  2nodd  43956  smndex1n0mnd  44012  lindslinindsimp1  44440  line2ylem  44666  line2xlem  44668
  Copyright terms: Public domain W3C validator