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

Theorem mtbird 313
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 217 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 187 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194
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 195
This theorem is referenced by:  eqneltrd  2706  nelsnOLD  4159  eqnbrtrd  4595  nsuceq0  5707  fvun1  6163  tz7.44-2  7367  oeeulem  7545  onomeneq  8012  supgtoreq  8236  inflb  8255  cantnfp1lem2  8436  cantnflem1  8446  rankxpsuc  8605  cardaleph  8772  cfsuc  8939  cflim2  8945  addnidpi  9579  genpnnp  9683  supaddc  10839  supmul1  10841  indstr2  11601  zbtwnre  11620  xrltnsym  11807  xrlttr  11810  xralrple  11871  supicclub2  12152  flltnz  12431  hashf1lem1  13050  swrdnd  13232  swrd0  13234  sqrtneglem  13803  rlimno1  14180  binomlem  14348  fprodn0f  14509  ruclem12  14757  dvdsle  14818  2tp1odd  14862  smu01lem  14993  rpexp  15218  oddprm  15301  pythagtriplem11  15316  pythagtriplem13  15318  pcpremul  15334  pczndvds  15355  pczndvds2  15357  pc2dvds  15369  pcadd  15379  pcmpt  15382  sgrp2nmndlem5  17187  pmtrdifellem4  17670  psgnunilem1  17684  psgnunilem2  17686  efgredlemc  17929  prmcyg  18066  ablfacrplem  18235  ablfac1eulem  18242  islbs2  18923  fidomndrng  19076  frlmssuvc2  19900  1stccnp  21022  fbasfip  21429  recld2  22372  metnrmlem1a  22416  xrhmeo  22500  bndth  22512  ioombl1lem4  23080  itg2seq  23259  itg2cnlem2  23279  dgrub  23738  dgrlb  23740  dgrnznn  23751  aaliou2  23843  taylthlem2  23876  dvlog2lem  24142  cxple2  24187  mumullem2  24650  chtub  24681  lgsval2lem  24776  lgsdir  24801  lgsne0  24804  lgsqr  24820  lgseisenlem1  24844  lgseisenlem2  24845  lgseisenlem4  24847  lgsquadlem1  24849  lgsquad2  24855  m1lgs  24857  2sqlem7  24893  2sqblem  24900  legso  25239  mirbtwnhl  25320  lmiopp  25439  axlowdimlem6  25572  usgra1v  25712  nbgranself  25756  cyclnspth  25952  eupath2lem3  26299  frgra2v  26319  frgrancvvdeqlem1  26350  2spotiundisj  26382  hmdmadj  27976  strlem1  28286  isoun  28655  archirng  28866  esumrnmpt2  29250  ballotlem4  29680  signswmnd  29753  signslema  29758  bnj1417  30156  tailfb  31335  unblimceq0  31461  unbdqndv2lem2  31464  topdifinffinlem  32154  icorempt2  32158  finxpreclem6  32192  mblfinlem4  32402  3dimlem2  33546  3dimlem3a  33547  3dimlem3OLDN  33549  3dim2  33555  3dim3  33556  lplnnle2at  33628  lplnnlelln  33630  llncvrlpln  33645  lvolnle3at  33669  lvolnlelln  33671  lvolnlelpln  33672  4atlem3  33683  lplncvrlvol  33703  dalem30  33789  dalem35  33794  lhp2at0nle  34122  4atexlemswapqr  34150  ltrncnvel  34229  trlnle  34274  cdleme35sn3a  34548  cdleme46frvlpq  34593  cdlemeg46c  34602  cdlemeg46nlpq  34606  cdleme48gfv  34626  cdlemg7fvbwN  34696  cdlemg4d  34702  cdlemg10a  34729  cdlemg12d  34735  cdlemg27b  34785  cdlemg31d  34789  dihmeetlem6  35399  dochshpsat  35544  dochexmidlem1  35550  mapdindp  35761  lspindp5  35860  cmpfiiin  36061  fnwe2lem2  36422  relexpmulg  36804  relexp01min  36807  relexpxpmin  36811  cvgdvgrat  37317  nelrnmpt  38066  difmap  38177  rnmptn0  38191  gtnelioc  38342  ltnelicc  38349  gtnelicc  38352  lenelioc  38393  xrgtnelicc  38395  limciccioolb  38471  limcrecl  38479  limcicciooub  38487  limclner  38501  reclimc  38503  sinaover2ne0  38534  icccncfext  38556  jumpncnp  38567  dvmptdiv  38590  itgsincmulx  38649  stoweidlem26  38702  stoweidlem35  38711  stirlinglem5  38754  dirker2re  38768  dirkerdenne0  38769  dirkertrigeqlem3  38776  dirkertrigeq  38777  dirkercncflem1  38779  dirkercncflem2  38780  dirkercncflem4  38782  fourierdlem10  38793  fourierdlem24  38807  fourierdlem25  38808  fourierdlem42  38825  fourierdlem44  38827  fourierdlem53  38835  fourierdlem58  38840  fourierdlem62  38844  fourierdlem76  38858  fourierdlem88  38870  fourierdlem104  38886  etransclem41  38951  etransclem44  38954  hoiqssbllem3  39297  fmtnoinf  39770  lighneallem3  39846  lighneallem4  39849  bits0eALTV  39913  oddprmALTV  39920  1loopgrvd0  40700  1egrvtxdg0  40708  nfrgr2v  41423  frgrncvvdeqlem1  41450  0nodd  41581  2nodd  41583  lindslinindsimp1  42021
  Copyright terms: Public domain W3C validator