Theorem mtbird 328

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

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

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 210

This theorem is referenced by:  eqneltrd  2909  eqnbrtrd  5048  nsuceq0  6239  fvun1  6729  tz7.44-2  8026  oeeulem  8210  onomeneq  8693  supgtoreq  8918  inflb  8937  cantnfp1lem2  9126  cantnflem1  9136  rankxpsuc  9295  cardaleph  9500  cfsuc  9668  cflim2  9674  addnidpi  10312  genpnnp  10416  supaddc  11595  supmul1  11597  nnneneg  11660  indstr2  12315  zbtwnre  12334  xrltnsym  12518  xrlttr  12521  xralrple  12586  supicclub2  12882  flltnz  13176  hashelne0d  13725  hashf1lem1  13809  swrdnd  14007  swrd0  14011  sqrtneglem  14618  rlimno1  15002  binomlem  15176  fprodn0f  15337  ruclem12  15586  dvdsle  15652  2tp1odd  15693  smu01lem  15824  rpexp  16054  oddprm  16137  pythagtriplem11  16152  pythagtriplem13  16154  pcpremul  16170  pczndvds2  16193  pc2dvds  16205  pcmpt  16218  smndex1n0mnd  18069  sgrp2nmndlem5  18086  pmtrdifellem4  18599  psgnunilem1  18613  psgnunilem2  18615  efgredlemc  18863  prmcyg  19007  ablfacrplem  19180  ablfac1eulem  19187  ablsimpgfindlem1  19222  islbs2  19919  fidomndrng  20073  frlmssuvc2  20484  1stccnp  22067  fbasfip  22473  metnrmlem1a  23463  xrhmeo  23551  bndth  23563  ioombl1lem4  24165  itg2seq  24346  dvmptdiv  24577  dgrlb  24833  dgrnznn  24844  aaliou2  24936  taylthlem2  24969  cos02pilt1  25118  dvlog2lem  25243  cxple2  25288  mumullem2  25765  chtub  25796  lgsval2lem  25891  lgsdir  25916  lgsne0  25919  lgsqr  25935  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem4  25962  lgsquadlem1  25964  lgsquad2  25970  m1lgs  25972  2sqlem7  26008  2sqblem  26015  legso  26393  lmiopp  26596  axlowdimlem6  26741  elntg2  26779  1loopgrvd0  27294  1egrvtxdg0  27301  nfrgr2v  28057  hmdmadj  29723  strlem1  30033  isoun  30461  archirng  30867  esumrnmpt2  31437  ballotlem4  31866  signswmnd  31937  signslema  31942  bnj1417  32423  satf0n0  32738  fmlaomn0  32750  prv1n  32791  nosupbnd1lem1  33321  nosupbnd2  33329  tailfb  33838  unblimceq0  33959  unbdqndv2lem2  33962  topdifinffinlem  34764  icorempo  34768  finxpreclem6  34813  lindsadd  35050  mblfinlem4  35097  3dimlem2  36755  3dimlem3a  36756  3dimlem3OLDN  36758  3dim2  36764  3dim3  36765  lplnnle2at  36837  lplnnlelln  36839  llncvrlpln  36854  lvolnle3at  36878  lvolnlelln  36880  lvolnlelpln  36881  4atlem3  36892  lplncvrlvol  36912  dalem30  36998  dalem35  37003  lhp2at0nle  37331  4atexlemswapqr  37359  ltrncnvel  37438  trlnle  37482  cdleme35sn3a  37755  cdleme46frvlpq  37800  cdlemeg46c  37809  cdlemeg46nlpq  37813  cdleme48gfv  37833  cdlemg7fvbwN  37903  cdlemg4d  37909  cdlemg10a  37936  cdlemg12d  37942  cdlemg27b  37992  cdlemg31d  37996  dihmeetlem6  38605  dochshpsat  38750  dochexmidlem1  38756  mapdindp  38967  lspindp5  39066  metakunt30  39379  xppss12  39409  oexpreposd  39487  dffltz  39615  cmpfiiin  39638  fnwe2lem2  39995  relexpmulg  40411  relexp01min  40414  relexpxpmin  40418  cvgdvgrat  41017  nelrnmpt  41720  difmap  41836  rnmptn0  41850  gtnelioc  42128  ltnelicc  42134  gtnelicc  42137  lenelioc  42173  xrgtnelicc  42175  limciccioolb  42263  limcrecl  42271  limcicciooub  42279  limclner  42293  reclimc  42295  sinaover2ne0  42510  icccncfext  42529  jumpncnp  42540  itgsincmulx  42616  stoweidlem26  42668  stoweidlem35  42677  stirlinglem5  42720  dirker2re  42734  dirkerdenne0  42735  dirkertrigeqlem3  42742  dirkertrigeq  42743  dirkercncflem1  42745  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem10  42759  fourierdlem24  42773  fourierdlem25  42774  fourierdlem42  42791  fourierdlem44  42793  fourierdlem53  42801  fourierdlem58  42806  fourierdlem62  42810  fourierdlem76  42824  fourierdlem88  42836  fourierdlem104  42852  etransclem41  42917  etransclem44  42920  hoiqssbllem3  43263  smfmbfcex  43393  ichnreuop  43989  fmtnoinf  44053  lighneallem3  44125  lighneallem4  44128  bits0eALTV  44198  oddprmALTV  44205  0nodd  44430  2nodd  44432  lindslinindsimp1  44866  line2ylem  45165  line2xlem  45167