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

Theorem mtbird 325
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  5124  rnmptn0  6197  nsuceq0  6401  fvun1  6933  tz7.44-2  8354  oeeulem  8549  onomeneqOLD  9174  supgtoreq  9407  inflb  9426  cantnfp1lem2  9616  cantnflem1  9626  rankxpsuc  9819  cardaleph  10026  cfsuc  10194  cflim2  10200  addnidpi  10838  genpnnp  10942  supaddc  12123  supmul1  12125  nnneneg  12189  indstr2  12853  zbtwnre  12872  xrltnsym  13057  xrlttr  13060  xralrple  13125  supicclub2  13422  flltnz  13717  hashelne0d  14269  hashf1lem1  14354  hashf1lem1OLD  14355  swrdnd  14543  swrd0  14547  sqrtneglem  15152  rlimno1  15539  binomlem  15715  fprodn0f  15875  ruclem12  16124  dvdsle  16193  2tp1odd  16235  smu01lem  16366  rpexp  16599  oddprm  16683  pythagtriplem11  16698  pythagtriplem13  16700  pcpremul  16716  pczndvds2  16740  pc2dvds  16752  pcmpt  16765  smndex1n0mnd  18723  sgrp2nmndlem5  18740  pmtrdifellem4  19262  psgnunilem1  19276  psgnunilem2  19278  efgredlemc  19528  prmcyg  19672  ablfacrplem  19845  ablfac1eulem  19852  ablsimpgfindlem1  19887  islbs2  20618  fidomndrng  20781  frlmssuvc2  21204  1stccnp  22816  fbasfip  23222  metnrmlem1a  24224  xrhmeo  24312  bndth  24324  ioombl1lem4  24928  itg2seq  25110  dvmptdiv  25341  dgrlb  25600  dgrnznn  25611  aaliou2  25703  taylthlem2  25736  cos02pilt1  25885  dvlog2lem  26010  cxple2  26055  mumullem2  26532  chtub  26563  lgsval2lem  26658  lgsdir  26683  lgsne0  26686  lgsqr  26702  lgseisenlem1  26726  lgseisenlem2  26727  lgseisenlem4  26729  lgsquadlem1  26731  lgsquad2  26737  m1lgs  26739  2sqlem7  26775  2sqblem  26782  nosupbnd1lem1  27059  nosupbnd2  27067  noinfbnd1lem1  27074  noinfbnd2lem1  27081  noinfbnd2  27082  legso  27544  lmiopp  27747  axlowdimlem6  27899  elntg2  27937  1loopgrvd0  28455  1egrvtxdg0  28462  nfrgr2v  29219  hmdmadj  30885  strlem1  31195  isoun  31618  archirng  32027  esumrnmpt2  32670  ballotlem4  33101  signswmnd  33172  signslema  33177  bnj1417  33656  satf0n0  33975  fmlaomn0  33987  prv1n  34028  tailfb  34852  unblimceq0  34973  unbdqndv2lem2  34976  topdifinffinlem  35821  icorempo  35825  finxpreclem6  35870  lindsadd  36074  mblfinlem4  36121  3dimlem2  37925  3dimlem3a  37926  3dimlem3OLDN  37928  3dim2  37934  3dim3  37935  lplnnle2at  38007  lplnnlelln  38009  llncvrlpln  38024  lvolnle3at  38048  lvolnlelln  38050  lvolnlelpln  38051  4atlem3  38062  lplncvrlvol  38082  dalem30  38168  dalem35  38173  lhp2at0nle  38501  4atexlemswapqr  38529  ltrncnvel  38608  trlnle  38652  cdleme35sn3a  38925  cdleme46frvlpq  38970  cdlemeg46c  38979  cdlemeg46nlpq  38983  cdleme48gfv  39003  cdlemg7fvbwN  39073  cdlemg4d  39079  cdlemg10a  39106  cdlemg12d  39112  cdlemg27b  39162  cdlemg31d  39166  dihmeetlem6  39775  dochshpsat  39920  dochexmidlem1  39926  mapdindp  40137  lspindp5  40236  dvrelog2b  40526  aks4d1p1p7  40534  aks4d1p6  40541  aks6d1c2p2  40552  metakunt30  40609  xppss12  40655  oexpreposd  40810  dffltz  40975  cmpfiiin  41023  fnwe2lem2  41381  oninfint  41573  dflim5  41666  relexpmulg  41989  relexp01min  41992  relexpxpmin  41996  cvgdvgrat  42600  nelrnmpt  43301  difmap  43435  gtnelioc  43736  ltnelicc  43742  gtnelicc  43745  lenelioc  43781  xrgtnelicc  43783  limciccioolb  43869  limcrecl  43877  limcicciooub  43885  limclner  43899  reclimc  43901  sinaover2ne0  44116  icccncfext  44135  jumpncnp  44146  itgsincmulx  44222  stoweidlem26  44274  stoweidlem35  44283  stirlinglem5  44326  dirker2re  44340  dirkerdenne0  44341  dirkertrigeqlem3  44348  dirkertrigeq  44349  dirkercncflem1  44351  dirkercncflem2  44352  dirkercncflem4  44354  fourierdlem10  44365  fourierdlem24  44379  fourierdlem25  44380  fourierdlem42  44397  fourierdlem44  44399  fourierdlem53  44407  fourierdlem58  44412  fourierdlem62  44416  fourierdlem76  44430  fourierdlem88  44442  fourierdlem104  44458  etransclem41  44523  etransclem44  44526  hoiqssbllem3  44872  smfmbfcex  45008  fsetprcnexALT  45303  ichnreuop  45671  fmtnoinf  45735  lighneallem3  45806  lighneallem4  45809  bits0eALTV  45879  oddprmALTV  45886  0nodd  46111  2nodd  46113  lindslinindsimp1  46545  line2ylem  46844  line2xlem  46846
  Copyright terms: Public domain W3C validator