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

Theorem mtbird 327
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 231 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 200 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208
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 209
This theorem is referenced by:  eqneltrd  2932  eqnbrtrd  5076  nsuceq0  6265  fvun1  6748  tz7.44-2  8037  oeeulem  8221  onomeneq  8702  supgtoreq  8928  inflb  8947  cantnfp1lem2  9136  cantnflem1  9146  rankxpsuc  9305  cardaleph  9509  cfsuc  9673  cflim2  9679  addnidpi  10317  genpnnp  10421  supaddc  11602  supmul1  11604  nnneneg  11666  indstr2  12321  zbtwnre  12340  xrltnsym  12524  xrlttr  12527  xralrple  12592  supicclub2  12883  flltnz  13175  hashelne0d  13723  hashf1lem1  13807  swrdnd  14010  swrd0  14014  sqrtneglem  14620  rlimno1  15004  binomlem  15178  fprodn0f  15339  ruclem12  15588  dvdsle  15654  2tp1odd  15695  smu01lem  15828  rpexp  16058  oddprm  16141  pythagtriplem11  16156  pythagtriplem13  16158  pcpremul  16174  pczndvds2  16197  pc2dvds  16209  pcmpt  16222  smndex1n0mnd  18071  sgrp2nmndlem5  18088  pmtrdifellem4  18601  psgnunilem1  18615  psgnunilem2  18617  efgredlemc  18865  prmcyg  19008  ablfacrplem  19181  ablfac1eulem  19188  ablsimpgfindlem1  19223  islbs2  19920  fidomndrng  20074  frlmssuvc2  20933  1stccnp  22064  fbasfip  22470  metnrmlem1a  23460  xrhmeo  23544  bndth  23556  ioombl1lem4  24156  itg2seq  24337  dvmptdiv  24565  dgrlb  24820  dgrnznn  24831  aaliou2  24923  taylthlem2  24956  cos02pilt1  25105  dvlog2lem  25229  cxple2  25274  mumullem2  25751  chtub  25782  lgsval2lem  25877  lgsdir  25902  lgsne0  25905  lgsqr  25921  lgseisenlem1  25945  lgseisenlem2  25946  lgseisenlem4  25948  lgsquadlem1  25950  lgsquad2  25956  m1lgs  25958  2sqlem7  25994  2sqblem  26001  legso  26379  lmiopp  26582  axlowdimlem6  26727  elntg2  26765  1loopgrvd0  27280  1egrvtxdg0  27287  nfrgr2v  28045  hmdmadj  29711  strlem1  30021  isoun  30431  archirng  30812  esumrnmpt2  31322  ballotlem4  31751  signswmnd  31822  signslema  31827  bnj1417  32308  satf0n0  32620  fmlaomn0  32632  prv1n  32673  nosupbnd1lem1  33203  nosupbnd2  33211  tailfb  33720  unblimceq0  33841  unbdqndv2lem2  33844  topdifinffinlem  34622  icorempo  34626  finxpreclem6  34671  lindsadd  34879  mblfinlem4  34926  3dimlem2  36589  3dimlem3a  36590  3dimlem3OLDN  36592  3dim2  36598  3dim3  36599  lplnnle2at  36671  lplnnlelln  36673  llncvrlpln  36688  lvolnle3at  36712  lvolnlelln  36714  lvolnlelpln  36715  4atlem3  36726  lplncvrlvol  36746  dalem30  36832  dalem35  36837  lhp2at0nle  37165  4atexlemswapqr  37193  ltrncnvel  37272  trlnle  37316  cdleme35sn3a  37589  cdleme46frvlpq  37634  cdlemeg46c  37643  cdlemeg46nlpq  37647  cdleme48gfv  37667  cdlemg7fvbwN  37737  cdlemg4d  37743  cdlemg10a  37770  cdlemg12d  37776  cdlemg27b  37826  cdlemg31d  37830  dihmeetlem6  38439  dochshpsat  38584  dochexmidlem1  38590  mapdindp  38801  lspindp5  38900  xppss12  39108  oexpreposd  39172  dffltz  39264  cmpfiiin  39287  fnwe2lem2  39644  relexpmulg  40048  relexp01min  40051  relexpxpmin  40055  cvgdvgrat  40638  nelrnmpt  41341  difmap  41463  rnmptn0  41477  gtnelioc  41758  ltnelicc  41765  gtnelicc  41768  lenelioc  41805  xrgtnelicc  41807  limciccioolb  41895  limcrecl  41903  limcicciooub  41911  limclner  41925  reclimc  41927  sinaover2ne0  42142  icccncfext  42163  jumpncnp  42174  itgsincmulx  42252  stoweidlem26  42305  stoweidlem35  42314  stirlinglem5  42357  dirker2re  42371  dirkerdenne0  42372  dirkertrigeqlem3  42379  dirkertrigeq  42380  dirkercncflem1  42382  dirkercncflem2  42383  dirkercncflem4  42385  fourierdlem10  42396  fourierdlem24  42410  fourierdlem25  42411  fourierdlem42  42428  fourierdlem44  42430  fourierdlem53  42438  fourierdlem58  42443  fourierdlem62  42447  fourierdlem76  42461  fourierdlem88  42473  fourierdlem104  42489  etransclem41  42554  etransclem44  42557  hoiqssbllem3  42900  ichnreuop  43628  fmtnoinf  43692  lighneallem3  43766  lighneallem4  43769  bits0eALTV  43839  oddprmALTV  43846  0nodd  44071  2nodd  44073  lindslinindsimp1  44506  line2ylem  44732  line2xlem  44734
  Copyright terms: Public domain W3C validator