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  2849  eqnbrtrd  5128  rnmptn0  6220  nsuceq0  6420  fvun1  6955  tz7.44-2  8378  oeeulem  8568  supgtoreq  9429  inflb  9448  cantnfp1lem2  9639  cantnflem1  9649  rankxpsuc  9842  cardaleph  10049  cfsuc  10217  cflim2  10223  addnidpi  10861  genpnnp  10965  supaddc  12157  supmul1  12159  nnneneg  12228  indstr2  12893  zbtwnre  12912  xrltnsym  13104  xrlttr  13107  xralrple  13172  supicclub2  13472  flltnz  13780  hashelne0d  14340  hashf1lem1  14427  swrdnd  14626  swrd0  14630  sqrtneglem  15239  rlimno1  15627  binomlem  15802  fprodn0f  15964  ruclem12  16216  dvdsle  16287  2tp1odd  16329  smu01lem  16462  rpexp  16699  oddprm  16788  pythagtriplem11  16803  pythagtriplem13  16805  pcpremul  16821  pczndvds2  16845  pc2dvds  16857  pcmpt  16870  smndex1n0mnd  18846  sgrp2nmndlem5  18863  pmtrdifellem4  19416  psgnunilem1  19430  psgnunilem2  19432  efgredlemc  19682  prmcyg  19831  ablfacrplem  20004  ablfac1eulem  20011  ablsimpgfindlem1  20046  fidomndrng  20689  islbs2  21071  frlmssuvc2  21711  1stccnp  23356  fbasfip  23762  metnrmlem1a  24754  xrhmeo  24851  bndth  24864  ioombl1lem4  25469  itg2seq  25650  dvmptdiv  25885  dgrlb  26148  dgrnznn  26159  aaliou2  26255  taylthlem2  26289  taylthlem2OLD  26290  cos02pilt1  26442  dvlog2lem  26568  cxple2  26613  mumullem2  27097  chtub  27130  lgsval2lem  27225  lgsdir  27250  lgsne0  27253  lgsqr  27269  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem4  27296  lgsquadlem1  27298  lgsquad2  27304  m1lgs  27306  2sqlem7  27342  2sqblem  27349  nosupbnd1lem1  27627  nosupbnd2  27635  noinfbnd1lem1  27642  noinfbnd2lem1  27649  noinfbnd2  27650  0elold  27828  sltmul2  28081  legso  28533  lmiopp  28736  axlowdimlem6  28881  elntg2  28919  1loopgrvd0  29439  1egrvtxdg0  29446  nfrgr2v  30208  nrt2irr  30409  hmdmadj  31876  strlem1  32186  isoun  32632  expgt0b  32748  archirng  33149  rsprprmprmidl  33500  rprmdvdsprod  33512  constrcon  33771  esumrnmpt2  34065  ballotlem4  34497  signswmnd  34555  signslema  34560  bnj1417  35038  satf0n0  35372  fmlaomn0  35384  prv1n  35425  tailfb  36372  weiunfr  36462  unblimceq0  36502  unbdqndv2lem2  36505  topdifinffinlem  37342  icorempo  37346  finxpreclem6  37391  lindsadd  37614  mblfinlem4  37661  3dimlem2  39460  3dimlem3a  39461  3dimlem3OLDN  39463  3dim2  39469  3dim3  39470  lplnnle2at  39542  lplnnlelln  39544  llncvrlpln  39559  lvolnle3at  39583  lvolnlelln  39585  lvolnlelpln  39586  4atlem3  39597  lplncvrlvol  39617  dalem30  39703  dalem35  39708  lhp2at0nle  40036  4atexlemswapqr  40064  ltrncnvel  40143  trlnle  40187  cdleme35sn3a  40460  cdleme46frvlpq  40505  cdlemeg46c  40514  cdlemeg46nlpq  40518  cdleme48gfv  40538  cdlemg7fvbwN  40608  cdlemg4d  40614  cdlemg10a  40641  cdlemg12d  40647  cdlemg27b  40697  cdlemg31d  40701  dihmeetlem6  41310  dochshpsat  41455  dochexmidlem1  41461  mapdindp  41672  lspindp5  41771  dvrelog2b  42061  aks4d1p1p7  42069  aks4d1p6  42076  aks6d1c2p2  42114  aks6d1c5lem1  42131  aks6d1c7lem1  42175  aks6d1c7  42179  xppss12  42224  oexpreposd  42317  mulltgt0d  42477  mullt0b2d  42479  sn-mullt0d  42480  dffltz  42629  cmpfiiin  42692  fnwe2lem2  43047  oninfint  43232  dflim5  43325  relexpmulg  43706  relexp01min  43709  relexpxpmin  43713  cvgdvgrat  44309  nelrnmpt  45085  difmap  45208  gtnelioc  45496  ltnelicc  45502  gtnelicc  45505  lenelioc  45541  xrgtnelicc  45543  limciccioolb  45626  limcrecl  45634  limcicciooub  45642  limclner  45656  reclimc  45658  sinaover2ne0  45873  icccncfext  45892  jumpncnp  45903  itgsincmulx  45979  stoweidlem26  46031  stoweidlem35  46040  stirlinglem5  46083  dirker2re  46097  dirkerdenne0  46098  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncflem1  46108  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem10  46122  fourierdlem24  46136  fourierdlem25  46137  fourierdlem42  46154  fourierdlem44  46156  fourierdlem53  46164  fourierdlem58  46169  fourierdlem62  46173  fourierdlem76  46187  fourierdlem88  46199  fourierdlem104  46215  etransclem41  46280  etransclem44  46283  hoiqssbllem3  46629  smfmbfcex  46765  fsetprcnexALT  47067  difltmodne  47347  minusmodnep2tmod  47358  modm1p1ne  47375  ichnreuop  47477  fmtnoinf  47541  lighneallem3  47612  lighneallem4  47615  bits0eALTV  47685  oddprmALTV  47692  upgrimpths  47913  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpg3kgrtriexlem5  48082  0nodd  48162  2nodd  48164  lindslinindsimp1  48450  line2ylem  48744  line2xlem  48746