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

Theorem mtbird 314
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 219 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 189 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196
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 197
This theorem is referenced by:  eqneltrd  2749  eqnbrtrd  4703  nsuceq0  5843  fvun1  6308  tz7.44-2  7548  oeeulem  7726  onomeneq  8191  supgtoreq  8417  inflb  8436  cantnfp1lem2  8614  cantnflem1  8624  rankxpsuc  8783  cardaleph  8950  cfsuc  9117  cflim2  9123  addnidpi  9761  genpnnp  9865  supaddc  11028  supmul1  11030  indstr2  11805  zbtwnre  11824  xrltnsym  12008  xrlttr  12011  xralrple  12074  supicclub2  12361  flltnz  12652  hashf1lem1  13277  swrdnd  13478  swrd0  13480  sqrtneglem  14051  rlimno1  14428  binomlem  14605  fprodn0f  14766  ruclem12  15014  dvdsle  15079  2tp1odd  15123  smu01lem  15254  rpexp  15479  oddprm  15562  pythagtriplem11  15577  pythagtriplem13  15579  pcpremul  15595  pczndvds  15616  pczndvds2  15618  pc2dvds  15630  pcadd  15640  pcmpt  15643  sgrp2nmndlem5  17463  pmtrdifellem4  17945  psgnunilem1  17959  psgnunilem2  17961  efgredlemc  18204  prmcyg  18341  ablfacrplem  18510  ablfac1eulem  18517  islbs2  19202  fidomndrng  19355  frlmssuvc2  20182  1stccnp  21313  fbasfip  21719  recld2  22664  metnrmlem1a  22708  xrhmeo  22792  bndth  22804  ioombl1lem4  23375  itg2seq  23554  itg2cnlem2  23574  dvmptdiv  23782  dgrub  24035  dgrlb  24037  dgrnznn  24048  aaliou2  24140  taylthlem2  24173  dvlog2lem  24443  cxple2  24488  mumullem2  24951  chtub  24982  lgsval2lem  25077  lgsdir  25102  lgsne0  25105  lgsqr  25121  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem4  25148  lgsquadlem1  25150  lgsquad2  25156  m1lgs  25158  2sqlem7  25194  2sqblem  25201  legso  25539  mirbtwnhl  25620  lmiopp  25739  axlowdimlem6  25872  1loopgrvd0  26456  1egrvtxdg0  26463  nfrgr2v  27252  hmdmadj  28927  strlem1  29237  isoun  29607  archirng  29870  esumrnmpt2  30258  ballotlem4  30688  signswmnd  30762  signslema  30767  bnj1417  31235  nosupbnd1lem1  31979  nosupbnd2  31987  tailfb  32497  unblimceq0  32623  unbdqndv2lem2  32626  topdifinffinlem  33325  icorempt2  33329  finxpreclem6  33363  mblfinlem4  33579  3dimlem2  35063  3dimlem3a  35064  3dimlem3OLDN  35066  3dim2  35072  3dim3  35073  lplnnle2at  35145  lplnnlelln  35147  llncvrlpln  35162  lvolnle3at  35186  lvolnlelln  35188  lvolnlelpln  35189  4atlem3  35200  lplncvrlvol  35220  dalem30  35306  dalem35  35311  lhp2at0nle  35639  4atexlemswapqr  35667  ltrncnvel  35746  trlnle  35791  cdleme35sn3a  36064  cdleme46frvlpq  36109  cdlemeg46c  36118  cdlemeg46nlpq  36122  cdleme48gfv  36142  cdlemg7fvbwN  36212  cdlemg4d  36218  cdlemg10a  36245  cdlemg12d  36251  cdlemg27b  36301  cdlemg31d  36305  dihmeetlem6  36915  dochshpsat  37060  dochexmidlem1  37066  mapdindp  37277  lspindp5  37376  cmpfiiin  37577  fnwe2lem2  37938  relexpmulg  38319  relexp01min  38322  relexpxpmin  38326  cvgdvgrat  38829  nelrnmpt  39571  difmap  39713  rnmptn0  39727  gtnelioc  40030  ltnelicc  40037  gtnelicc  40040  lenelioc  40081  xrgtnelicc  40083  limciccioolb  40171  limcrecl  40179  limcicciooub  40187  limclner  40201  reclimc  40203  sinaover2ne0  40397  icccncfext  40418  jumpncnp  40429  itgsincmulx  40508  stoweidlem26  40561  stoweidlem35  40570  stirlinglem5  40613  dirker2re  40627  dirkerdenne0  40628  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkercncflem1  40638  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem10  40652  fourierdlem24  40666  fourierdlem25  40667  fourierdlem42  40684  fourierdlem44  40686  fourierdlem53  40694  fourierdlem58  40699  fourierdlem62  40703  fourierdlem76  40717  fourierdlem88  40729  fourierdlem104  40745  etransclem41  40810  etransclem44  40813  hoiqssbllem3  41159  fmtnoinf  41773  lighneallem3  41849  lighneallem4  41852  bits0eALTV  41916  oddprmALTV  41923  0nodd  42135  2nodd  42137  lindslinindsimp1  42571
  Copyright terms: Public domain W3C validator