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  2883  eqnbrtrd  5130  nelrnmpt  5959  rnmptn0  6247  nsuceq0  6448  fvun1  6974  tz7.44-2  8395  oeeulem  8588  supgtoreq  9432  inflb  9451  cantnfp1lem2  9649  cantnflem1  9659  rankxpsuc  9855  cardaleph  10074  cfsuc  10242  cflim2  10248  addnidpi  10887  genpnnp  10991  supaddc  12183  supmul1  12185  nnneneg  12272  indstr2  12952  zbtwnre  12971  xrltnsym  13163  xrlttr  13166  xralrple  13232  supicclub2  13532  flltnz  13846  hashelne0d  14406  hashf1lem1  14494  swrdnd  14694  swrd0  14698  sqrtneglem  15319  rlimno1  15707  binomlem  15885  fprodn0f  16047  ruclem12  16298  dvdsle  16369  2tp1odd  16411  smu01lem  16544  rpexp  16782  oddprm  16871  pythagtriplem11  16886  pythagtriplem13  16888  pcpremul  16904  pczndvds2  16928  pc2dvds  16940  pcmpt  16953  smndex1n0mnd  18975  sgrp2nmndlem5  18992  pmtrdifellem4  19550  psgnunilem1  19564  psgnunilem2  19566  efgredlemc  19816  prmcyg  19965  ablfacrplem  20138  ablfac1eulem  20145  ablsimpgfindlem1  20180  fidomndrng  20858  islbs2  21259  frlmssuvc2  21926  1stccnp  23600  fbasfip  24006  metnrmlem1a  24997  xrhmeo  25086  bndth  25098  ioombl1lem4  25701  itg2seq  25882  dvmptdiv  26114  dgrlb  26374  dgrnznn  26385  aaliou2  26482  taylthlem2  26515  cos02pilt1  26669  dvlog2lem  26795  cxple2  26840  mumullem2  27322  chtub  27354  lgsval2lem  27449  lgsdir  27474  lgsne0  27477  lgsqr  27493  lgseisenlem1  27517  lgseisenlem2  27518  lgseisenlem4  27520  lgsquadlem1  27522  lgsquad2  27528  m1lgs  27530  2sqlem7  27566  2sqblem  27573  nosupbnd1lem1  27850  nosupbnd2  27858  noinfbnd1lem1  27865  noinfbnd2lem1  27872  noinfbnd2  27873  0elold  28081  ltmuls2  28342  pw2cut2  28633  legso  28846  tgelrnpln  29036  plngrotlem2  29048  lmiopp  29090  axlowdimlem6  29275  elntg2  29313  1loopgrvd0  29832  1egrvtxdg0  29839  nfrgr2v  30601  nrt2irr  30802  hmdmadj  32270  strlem1  32580  isoun  33025  expgt0b  33139  archirng  33486  rsprprmprmidl  33790  rprmdvdsprod  33802  extdgfialglem1  34060  constrcon  34142  esumrnmpt2  34436  ballotlem4  34867  signswmnd  34922  signslema  34927  bnj1417  35407  satf0n0  35848  fmlaomn0  35860  prv1n  35901  tailfb  36866  weiunfr  36956  unblimceq0  37074  unbdqndv2lem2  37077  qdiff  37949  topdifinffinlem  37971  icorempo  37975  finxpreclem6  38020  lindsadd  38242  mblfinlem4  38289  3dimlem2  40211  3dimlem3a  40212  3dimlem3OLDN  40214  3dim2  40220  3dim3  40221  lplnnle2at  40293  lplnnlelln  40295  llncvrlpln  40310  lvolnle3at  40334  lvolnlelln  40336  lvolnlelpln  40337  4atlem3  40348  lplncvrlvol  40368  dalem30  40454  dalem35  40459  lhp2at0nle  40787  4atexlemswapqr  40815  ltrncnvel  40894  trlnle  40938  cdleme35sn3a  41211  cdleme46frvlpq  41256  cdlemeg46c  41265  cdlemeg46nlpq  41269  cdleme48gfv  41289  cdlemg7fvbwN  41359  cdlemg4d  41365  cdlemg10a  41392  cdlemg12d  41398  cdlemg27b  41448  cdlemg31d  41452  dihmeetlem6  42061  dochshpsat  42206  dochexmidlem1  42212  mapdindp  42423  lspindp5  42522  dvrelog2b  42811  aks4d1p1p7  42819  aks4d1p6  42826  aks6d1c2p2  42864  aks6d1c5lem1  42881  aks6d1c7lem1  42925  aks6d1c7  42929  xppss12  42978  oexpreposd  43061  mulltgt0d  43234  mullt0b2d  43236  sn-mullt0d  43237  dffltz  43346  cmpfiiin  43408  fnwe2lem2  43758  oninfint  43943  dflim5  44036  relexpmulg  44416  relexp01min  44419  relexpxpmin  44423  cvgdvgrat  45003  difmap  45903  gtnelioc  46187  ltnelicc  46193  gtnelicc  46196  lenelioc  46232  xrgtnelicc  46234  limciccioolb  46317  limcrecl  46325  limcicciooub  46331  limclner  46345  reclimc  46347  sinaover2ne0  46562  icccncfext  46581  jumpncnp  46592  itgsincmulx  46668  stoweidlem26  46720  stoweidlem35  46729  stirlinglem5  46772  dirker2re  46786  dirkerdenne0  46787  dirkertrigeqlem3  46794  dirkertrigeq  46795  dirkercncflem1  46797  dirkercncflem2  46798  dirkercncflem4  46800  fourierdlem10  46811  fourierdlem24  46825  fourierdlem25  46826  fourierdlem42  46843  fourierdlem44  46845  fourierdlem53  46853  fourierdlem58  46858  fourierdlem62  46862  fourierdlem76  46876  fourierdlem88  46888  fourierdlem104  46904  etransclem41  46969  etransclem44  46972  hoiqssbllem3  47318  smfmbfcex  47454  fsetprcnexALT  47776  difltmodne  48062  minusmodnep2tmod  48073  modm1p1ne  48090  ichnreuop  48198  fmtnoinf  48265  lighneallem3  48336  lighneallem4  48339  bits0eALTV  48422  oddprmALTV  48429  upgrimpths  48651  gpg5nbgrvtx03starlem1  48810  gpg5nbgrvtx03starlem2  48811  gpg5nbgrvtx03starlem3  48812  gpg5nbgrvtx13starlem1  48813  gpg5nbgrvtx13starlem2  48814  gpg5nbgrvtx13starlem3  48815  gpg3kgrtriexlem5  48829  gpg5edgnedg  48872  0nodd  48912  2nodd  48914  smprngprmrng  49081  lindslinindsimp1  49214  line2ylem  49508  line2xlem  49510