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

Step	Hyp	Ref	Expression
1		mtbird.min	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		mtbird.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimpd 229	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 198	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  eqneltrd  2848  eqnbrtrd  5125  rnmptn0  6217  nsuceq0  6417  fvun1  6952  tz7.44-2  8375  oeeulem  8565  supgtoreq  9422  inflb  9441  cantnfp1lem2  9632  cantnflem1  9642  rankxpsuc  9835  cardaleph  10042  cfsuc  10210  cflim2  10216  addnidpi  10854  genpnnp  10958  supaddc  12150  supmul1  12152  nnneneg  12221  indstr2  12886  zbtwnre  12905  xrltnsym  13097  xrlttr  13100  xralrple  13165  supicclub2  13465  flltnz  13773  hashelne0d  14333  hashf1lem1  14420  swrdnd  14619  swrd0  14623  sqrtneglem  15232  rlimno1  15620  binomlem  15795  fprodn0f  15957  ruclem12  16209  dvdsle  16280  2tp1odd  16322  smu01lem  16455  rpexp  16692  oddprm  16781  pythagtriplem11  16796  pythagtriplem13  16798  pcpremul  16814  pczndvds2  16838  pc2dvds  16850  pcmpt  16863  smndex1n0mnd  18839  sgrp2nmndlem5  18856  pmtrdifellem4  19409  psgnunilem1  19423  psgnunilem2  19425  efgredlemc  19675  prmcyg  19824  ablfacrplem  19997  ablfac1eulem  20004  ablsimpgfindlem1  20039  fidomndrng  20682  islbs2  21064  frlmssuvc2  21704  1stccnp  23349  fbasfip  23755  metnrmlem1a  24747  xrhmeo  24844  bndth  24857  ioombl1lem4  25462  itg2seq  25643  dvmptdiv  25878  dgrlb  26141  dgrnznn  26152  aaliou2  26248  taylthlem2  26282  taylthlem2OLD  26283  cos02pilt1  26435  dvlog2lem  26561  cxple2  26606  mumullem2  27090  chtub  27123  lgsval2lem  27218  lgsdir  27243  lgsne0  27246  lgsqr  27262  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem4  27289  lgsquadlem1  27291  lgsquad2  27297  m1lgs  27299  2sqlem7  27335  2sqblem  27342  nosupbnd1lem1  27620  nosupbnd2  27628  noinfbnd1lem1  27635  noinfbnd2lem1  27642  noinfbnd2  27643  0elold  27821  sltmul2  28074  legso  28526  lmiopp  28729  axlowdimlem6  28874  elntg2  28912  1loopgrvd0  29432  1egrvtxdg0  29439  nfrgr2v  30201  nrt2irr  30402  hmdmadj  31869  strlem1  32179  isoun  32625  expgt0b  32741  archirng  33142  rsprprmprmidl  33493  rprmdvdsprod  33505  constrcon  33764  esumrnmpt2  34058  ballotlem4  34490  signswmnd  34548  signslema  34553  bnj1417  35031  satf0n0  35365  fmlaomn0  35377  prv1n  35418  tailfb  36365  weiunfr  36455  unblimceq0  36495  unbdqndv2lem2  36498  topdifinffinlem  37335  icorempo  37339  finxpreclem6  37384  lindsadd  37607  mblfinlem4  37654  3dimlem2  39453  3dimlem3a  39454  3dimlem3OLDN  39456  3dim2  39462  3dim3  39463  lplnnle2at  39535  lplnnlelln  39537  llncvrlpln  39552  lvolnle3at  39576  lvolnlelln  39578  lvolnlelpln  39579  4atlem3  39590  lplncvrlvol  39610  dalem30  39696  dalem35  39701  lhp2at0nle  40029  4atexlemswapqr  40057  ltrncnvel  40136  trlnle  40180  cdleme35sn3a  40453  cdleme46frvlpq  40498  cdlemeg46c  40507  cdlemeg46nlpq  40511  cdleme48gfv  40531  cdlemg7fvbwN  40601  cdlemg4d  40607  cdlemg10a  40634  cdlemg12d  40640  cdlemg27b  40690  cdlemg31d  40694  dihmeetlem6  41303  dochshpsat  41448  dochexmidlem1  41454  mapdindp  41665  lspindp5  41764  dvrelog2b  42054  aks4d1p1p7  42062  aks4d1p6  42069  aks6d1c2p2  42107  aks6d1c5lem1  42124  aks6d1c7lem1  42168  aks6d1c7  42172  xppss12  42217  oexpreposd  42310  mulltgt0d  42470  mullt0b2d  42472  sn-mullt0d  42473  dffltz  42622  cmpfiiin  42685  fnwe2lem2  43040  oninfint  43225  dflim5  43318  relexpmulg  43699  relexp01min  43702  relexpxpmin  43706  cvgdvgrat  44302  nelrnmpt  45078  difmap  45201  gtnelioc  45489  ltnelicc  45495  gtnelicc  45498  lenelioc  45534  xrgtnelicc  45536  limciccioolb  45619  limcrecl  45627  limcicciooub  45635  limclner  45649  reclimc  45651  sinaover2ne0  45866  icccncfext  45885  jumpncnp  45896  itgsincmulx  45972  stoweidlem26  46024  stoweidlem35  46033  stirlinglem5  46076  dirker2re  46090  dirkerdenne0  46091  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem10  46115  fourierdlem24  46129  fourierdlem25  46130  fourierdlem42  46147  fourierdlem44  46149  fourierdlem53  46157  fourierdlem58  46162  fourierdlem62  46166  fourierdlem76  46180  fourierdlem88  46192  fourierdlem104  46208  etransclem41  46273  etransclem44  46276  hoiqssbllem3  46622  smfmbfcex  46758  fsetprcnexALT  47063  difltmodne  47343  minusmodnep2tmod  47354  modm1p1ne  47371  ichnreuop  47473  fmtnoinf  47537  lighneallem3  47608  lighneallem4  47611  bits0eALTV  47681  oddprmALTV  47688  upgrimpths  47909  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpg3kgrtriexlem5  48078  0nodd  48158  2nodd  48160  lindslinindsimp1  48446  line2ylem  48740  line2xlem  48742