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

Theorem mtbird 324
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 228 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 197 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205
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 206
This theorem is referenced by:  eqneltrd  2858  eqnbrtrd  5088  rnmptn0  6136  nsuceq0  6331  fvun1  6841  tz7.44-2  8209  oeeulem  8394  onomeneq  8943  supgtoreq  9159  inflb  9178  cantnfp1lem2  9367  cantnflem1  9377  rankxpsuc  9571  cardaleph  9776  cfsuc  9944  cflim2  9950  addnidpi  10588  genpnnp  10692  supaddc  11872  supmul1  11874  nnneneg  11938  indstr2  12596  zbtwnre  12615  xrltnsym  12800  xrlttr  12803  xralrple  12868  supicclub2  13165  flltnz  13459  hashelne0d  14011  hashf1lem1  14096  hashf1lem1OLD  14097  swrdnd  14295  swrd0  14299  sqrtneglem  14906  rlimno1  15293  binomlem  15469  fprodn0f  15629  ruclem12  15878  dvdsle  15947  2tp1odd  15989  smu01lem  16120  rpexp  16355  oddprm  16439  pythagtriplem11  16454  pythagtriplem13  16456  pcpremul  16472  pczndvds2  16496  pc2dvds  16508  pcmpt  16521  smndex1n0mnd  18466  sgrp2nmndlem5  18483  pmtrdifellem4  19002  psgnunilem1  19016  psgnunilem2  19018  efgredlemc  19266  prmcyg  19410  ablfacrplem  19583  ablfac1eulem  19590  ablsimpgfindlem1  19625  islbs2  20331  fidomndrng  20492  frlmssuvc2  20912  1stccnp  22521  fbasfip  22927  metnrmlem1a  23927  xrhmeo  24015  bndth  24027  ioombl1lem4  24630  itg2seq  24812  dvmptdiv  25043  dgrlb  25302  dgrnznn  25313  aaliou2  25405  taylthlem2  25438  cos02pilt1  25587  dvlog2lem  25712  cxple2  25757  mumullem2  26234  chtub  26265  lgsval2lem  26360  lgsdir  26385  lgsne0  26388  lgsqr  26404  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem4  26431  lgsquadlem1  26433  lgsquad2  26439  m1lgs  26441  2sqlem7  26477  2sqblem  26484  legso  26864  lmiopp  27067  axlowdimlem6  27218  elntg2  27256  1loopgrvd0  27774  1egrvtxdg0  27781  nfrgr2v  28537  hmdmadj  30203  strlem1  30513  isoun  30936  archirng  31344  esumrnmpt2  31936  ballotlem4  32365  signswmnd  32436  signslema  32441  bnj1417  32921  satf0n0  33240  fmlaomn0  33252  prv1n  33293  nosupbnd1lem1  33838  nosupbnd2  33846  noinfbnd1lem1  33853  noinfbnd2lem1  33860  noinfbnd2  33861  tailfb  34493  unblimceq0  34614  unbdqndv2lem2  34617  topdifinffinlem  35445  icorempo  35449  finxpreclem6  35494  lindsadd  35697  mblfinlem4  35744  3dimlem2  37400  3dimlem3a  37401  3dimlem3OLDN  37403  3dim2  37409  3dim3  37410  lplnnle2at  37482  lplnnlelln  37484  llncvrlpln  37499  lvolnle3at  37523  lvolnlelln  37525  lvolnlelpln  37526  4atlem3  37537  lplncvrlvol  37557  dalem30  37643  dalem35  37648  lhp2at0nle  37976  4atexlemswapqr  38004  ltrncnvel  38083  trlnle  38127  cdleme35sn3a  38400  cdleme46frvlpq  38445  cdlemeg46c  38454  cdlemeg46nlpq  38458  cdleme48gfv  38478  cdlemg7fvbwN  38548  cdlemg4d  38554  cdlemg10a  38581  cdlemg12d  38587  cdlemg27b  38637  cdlemg31d  38641  dihmeetlem6  39250  dochshpsat  39395  dochexmidlem1  39401  mapdindp  39612  lspindp5  39711  dvrelog2b  40002  aks4d1p1p7  40010  aks4d1p6  40017  metakunt30  40082  xppss12  40130  oexpreposd  40242  dffltz  40387  cmpfiiin  40435  fnwe2lem2  40792  relexpmulg  41207  relexp01min  41210  relexpxpmin  41214  cvgdvgrat  41820  nelrnmpt  42523  difmap  42636  gtnelioc  42919  ltnelicc  42925  gtnelicc  42928  lenelioc  42964  xrgtnelicc  42966  limciccioolb  43052  limcrecl  43060  limcicciooub  43068  limclner  43082  reclimc  43084  sinaover2ne0  43299  icccncfext  43318  jumpncnp  43329  itgsincmulx  43405  stoweidlem26  43457  stoweidlem35  43466  stirlinglem5  43509  dirker2re  43523  dirkerdenne0  43524  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncflem1  43534  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem10  43548  fourierdlem24  43562  fourierdlem25  43563  fourierdlem42  43580  fourierdlem44  43582  fourierdlem53  43590  fourierdlem58  43595  fourierdlem62  43599  fourierdlem76  43613  fourierdlem88  43625  fourierdlem104  43641  etransclem41  43706  etransclem44  43709  hoiqssbllem3  44052  smfmbfcex  44182  fsetprcnexALT  44443  ichnreuop  44812  fmtnoinf  44876  lighneallem3  44947  lighneallem4  44950  bits0eALTV  45020  oddprmALTV  45027  0nodd  45252  2nodd  45254  lindslinindsimp1  45686  line2ylem  45985  line2xlem  45987
  Copyright terms: Public domain W3C validator