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  2857  eqnbrtrd  5104  nelrnmpt  5916  rnmptn0  6202  nsuceq0  6402  fvun1  6925  tz7.44-2  8339  oeeulem  8530  supgtoreq  9377  inflb  9396  cantnfp1lem2  9591  cantnflem1  9601  rankxpsuc  9797  cardaleph  10002  cfsuc  10170  cflim2  10176  addnidpi  10815  genpnnp  10919  supaddc  12114  supmul1  12116  nnneneg  12203  indstr2  12868  zbtwnre  12887  xrltnsym  13079  xrlttr  13082  xralrple  13148  supicclub2  13448  flltnz  13761  hashelne0d  14321  hashf1lem1  14408  swrdnd  14608  swrd0  14612  sqrtneglem  15219  rlimno1  15607  binomlem  15785  fprodn0f  15947  ruclem12  16199  dvdsle  16270  2tp1odd  16312  smu01lem  16445  rpexp  16683  oddprm  16772  pythagtriplem11  16787  pythagtriplem13  16789  pcpremul  16805  pczndvds2  16829  pc2dvds  16841  pcmpt  16854  smndex1n0mnd  18874  sgrp2nmndlem5  18891  pmtrdifellem4  19445  psgnunilem1  19459  psgnunilem2  19461  efgredlemc  19711  prmcyg  19860  ablfacrplem  20033  ablfac1eulem  20040  ablsimpgfindlem1  20075  fidomndrng  20741  islbs2  21144  frlmssuvc2  21785  1stccnp  23437  fbasfip  23843  metnrmlem1a  24834  xrhmeo  24923  bndth  24935  ioombl1lem4  25538  itg2seq  25719  dvmptdiv  25951  dgrlb  26211  dgrnznn  26222  aaliou2  26317  taylthlem2  26351  taylthlem2OLD  26352  cos02pilt1  26503  dvlog2lem  26629  cxple2  26674  mumullem2  27157  chtub  27189  lgsval2lem  27284  lgsdir  27309  lgsne0  27312  lgsqr  27328  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem4  27355  lgsquadlem1  27357  lgsquad2  27363  m1lgs  27365  2sqlem7  27401  2sqblem  27408  nosupbnd1lem1  27686  nosupbnd2  27694  noinfbnd1lem1  27701  noinfbnd2lem1  27708  noinfbnd2  27709  0elold  27916  ltmuls2  28177  pw2cut2  28468  legso  28681  lmiopp  28884  axlowdimlem6  29030  elntg2  29068  1loopgrvd0  29588  1egrvtxdg0  29595  nfrgr2v  30357  nrt2irr  30558  hmdmadj  32026  strlem1  32336  isoun  32790  expgt0b  32905  archirng  33264  rsprprmprmidl  33597  rprmdvdsprod  33609  extdgfialglem1  33852  constrcon  33934  esumrnmpt2  34228  ballotlem4  34659  signswmnd  34717  signslema  34722  bnj1417  35199  satf0n0  35576  fmlaomn0  35588  prv1n  35629  tailfb  36575  weiunfr  36665  unblimceq0  36783  unbdqndv2lem2  36786  topdifinffinlem  37677  icorempo  37681  finxpreclem6  37726  lindsadd  37948  mblfinlem4  37995  3dimlem2  39919  3dimlem3a  39920  3dimlem3OLDN  39922  3dim2  39928  3dim3  39929  lplnnle2at  40001  lplnnlelln  40003  llncvrlpln  40018  lvolnle3at  40042  lvolnlelln  40044  lvolnlelpln  40045  4atlem3  40056  lplncvrlvol  40076  dalem30  40162  dalem35  40167  lhp2at0nle  40495  4atexlemswapqr  40523  ltrncnvel  40602  trlnle  40646  cdleme35sn3a  40919  cdleme46frvlpq  40964  cdlemeg46c  40973  cdlemeg46nlpq  40977  cdleme48gfv  40997  cdlemg7fvbwN  41067  cdlemg4d  41073  cdlemg10a  41100  cdlemg12d  41106  cdlemg27b  41156  cdlemg31d  41160  dihmeetlem6  41769  dochshpsat  41914  dochexmidlem1  41920  mapdindp  42131  lspindp5  42230  dvrelog2b  42519  aks4d1p1p7  42527  aks4d1p6  42534  aks6d1c2p2  42572  aks6d1c5lem1  42589  aks6d1c7lem1  42633  aks6d1c7  42637  xppss12  42684  oexpreposd  42768  mulltgt0d  42941  mullt0b2d  42943  sn-mullt0d  42944  dffltz  43081  cmpfiiin  43143  fnwe2lem2  43497  oninfint  43682  dflim5  43775  relexpmulg  44155  relexp01min  44158  relexpxpmin  44162  cvgdvgrat  44758  difmap  45654  gtnelioc  45939  ltnelicc  45945  gtnelicc  45948  lenelioc  45984  xrgtnelicc  45986  limciccioolb  46069  limcrecl  46077  limcicciooub  46083  limclner  46097  reclimc  46099  sinaover2ne0  46314  icccncfext  46333  jumpncnp  46344  itgsincmulx  46420  stoweidlem26  46472  stoweidlem35  46481  stirlinglem5  46524  dirker2re  46538  dirkerdenne0  46539  dirkertrigeqlem3  46546  dirkertrigeq  46547  dirkercncflem1  46549  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem10  46563  fourierdlem24  46577  fourierdlem25  46578  fourierdlem42  46595  fourierdlem44  46597  fourierdlem53  46605  fourierdlem58  46610  fourierdlem62  46614  fourierdlem76  46628  fourierdlem88  46640  fourierdlem104  46656  etransclem41  46721  etransclem44  46724  hoiqssbllem3  47070  smfmbfcex  47206  fsetprcnexALT  47522  difltmodne  47808  minusmodnep2tmod  47819  modm1p1ne  47836  ichnreuop  47944  fmtnoinf  48011  lighneallem3  48082  lighneallem4  48085  bits0eALTV  48168  oddprmALTV  48175  upgrimpths  48397  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpg3kgrtriexlem5  48575  gpg5edgnedg  48618  0nodd  48658  2nodd  48660  lindslinindsimp1  48945  line2ylem  49239  line2xlem  49241