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 228	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 197	1 ⊢ (𝜑 → ¬ 𝜓)

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  2854  eqnbrtrd  5167  rnmptn0  6244  nsuceq0  6448  fvun1  6983  tz7.44-2  8407  oeeulem  8601  onomeneqOLD  9229  supgtoreq  9465  inflb  9484  cantnfp1lem2  9674  cantnflem1  9684  rankxpsuc  9877  cardaleph  10084  cfsuc  10252  cflim2  10258  addnidpi  10896  genpnnp  11000  supaddc  12181  supmul1  12183  nnneneg  12247  indstr2  12911  zbtwnre  12930  xrltnsym  13116  xrlttr  13119  xralrple  13184  supicclub2  13481  flltnz  13776  hashelne0d  14328  hashf1lem1  14415  hashf1lem1OLD  14416  swrdnd  14604  swrd0  14608  sqrtneglem  15213  rlimno1  15600  binomlem  15775  fprodn0f  15935  ruclem12  16184  dvdsle  16253  2tp1odd  16295  smu01lem  16426  rpexp  16659  oddprm  16743  pythagtriplem11  16758  pythagtriplem13  16760  pcpremul  16776  pczndvds2  16800  pc2dvds  16812  pcmpt  16825  smndex1n0mnd  18793  sgrp2nmndlem5  18810  pmtrdifellem4  19347  psgnunilem1  19361  psgnunilem2  19363  efgredlemc  19613  prmcyg  19762  ablfacrplem  19935  ablfac1eulem  19942  ablsimpgfindlem1  19977  islbs2  20767  fidomndrng  20926  frlmssuvc2  21350  1stccnp  22966  fbasfip  23372  metnrmlem1a  24374  xrhmeo  24462  bndth  24474  ioombl1lem4  25078  itg2seq  25260  dvmptdiv  25491  dgrlb  25750  dgrnznn  25761  aaliou2  25853  taylthlem2  25886  cos02pilt1  26035  dvlog2lem  26160  cxple2  26205  mumullem2  26684  chtub  26715  lgsval2lem  26810  lgsdir  26835  lgsne0  26838  lgsqr  26854  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem4  26881  lgsquadlem1  26883  lgsquad2  26889  m1lgs  26891  2sqlem7  26927  2sqblem  26934  nosupbnd1lem1  27211  nosupbnd2  27219  noinfbnd1lem1  27226  noinfbnd2lem1  27233  noinfbnd2  27234  0elold  27402  sltmul2  27623  legso  27850  lmiopp  28053  axlowdimlem6  28205  elntg2  28243  1loopgrvd0  28761  1egrvtxdg0  28768  nfrgr2v  29525  nrt2irr  29726  hmdmadj  31193  strlem1  31503  isoun  31923  archirng  32334  esumrnmpt2  33066  ballotlem4  33497  signswmnd  33568  signslema  33573  bnj1417  34052  satf0n0  34369  fmlaomn0  34381  prv1n  34422  tailfb  35262  unblimceq0  35383  unbdqndv2lem2  35386  topdifinffinlem  36228  icorempo  36232  finxpreclem6  36277  lindsadd  36481  mblfinlem4  36528  3dimlem2  38330  3dimlem3a  38331  3dimlem3OLDN  38333  3dim2  38339  3dim3  38340  lplnnle2at  38412  lplnnlelln  38414  llncvrlpln  38429  lvolnle3at  38453  lvolnlelln  38455  lvolnlelpln  38456  4atlem3  38467  lplncvrlvol  38487  dalem30  38573  dalem35  38578  lhp2at0nle  38906  4atexlemswapqr  38934  ltrncnvel  39013  trlnle  39057  cdleme35sn3a  39330  cdleme46frvlpq  39375  cdlemeg46c  39384  cdlemeg46nlpq  39388  cdleme48gfv  39408  cdlemg7fvbwN  39478  cdlemg4d  39484  cdlemg10a  39511  cdlemg12d  39517  cdlemg27b  39567  cdlemg31d  39571  dihmeetlem6  40180  dochshpsat  40325  dochexmidlem1  40331  mapdindp  40542  lspindp5  40641  dvrelog2b  40931  aks4d1p1p7  40939  aks4d1p6  40946  aks6d1c2p2  40957  metakunt30  41014  xppss12  41047  oexpreposd  41212  dffltz  41376  cmpfiiin  41435  fnwe2lem2  41793  oninfint  41985  dflim5  42079  relexpmulg  42461  relexp01min  42464  relexpxpmin  42468  cvgdvgrat  43072  nelrnmpt  43773  difmap  43906  gtnelioc  44204  ltnelicc  44210  gtnelicc  44213  lenelioc  44249  xrgtnelicc  44251  limciccioolb  44337  limcrecl  44345  limcicciooub  44353  limclner  44367  reclimc  44369  sinaover2ne0  44584  icccncfext  44603  jumpncnp  44614  itgsincmulx  44690  stoweidlem26  44742  stoweidlem35  44751  stirlinglem5  44794  dirker2re  44808  dirkerdenne0  44809  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkercncflem1  44819  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem10  44833  fourierdlem24  44847  fourierdlem25  44848  fourierdlem42  44865  fourierdlem44  44867  fourierdlem53  44875  fourierdlem58  44880  fourierdlem62  44884  fourierdlem76  44898  fourierdlem88  44910  fourierdlem104  44926  etransclem41  44991  etransclem44  44994  hoiqssbllem3  45340  smfmbfcex  45476  fsetprcnexALT  45772  ichnreuop  46140  fmtnoinf  46204  lighneallem3  46275  lighneallem4  46278  bits0eALTV  46348  oddprmALTV  46355  0nodd  46580  2nodd  46582  lindslinindsimp1  47138  line2ylem  47437  line2xlem  47439