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  2849  eqnbrtrd  5160  rnmptn0  6242  nsuceq0  6446  fvun1  6983  tz7.44-2  8421  oeeulem  8615  onomeneqOLD  9247  supgtoreq  9487  inflb  9506  cantnfp1lem2  9696  cantnflem1  9706  rankxpsuc  9899  cardaleph  10106  cfsuc  10274  cflim2  10280  addnidpi  10918  genpnnp  11022  supaddc  12205  supmul1  12207  nnneneg  12271  indstr2  12935  zbtwnre  12954  xrltnsym  13142  xrlttr  13145  xralrple  13210  supicclub2  13507  flltnz  13802  hashelne0d  14353  hashf1lem1  14441  hashf1lem1OLD  14442  swrdnd  14630  swrd0  14634  sqrtneglem  15239  rlimno1  15626  binomlem  15801  fprodn0f  15961  ruclem12  16211  dvdsle  16280  2tp1odd  16322  smu01lem  16453  rpexp  16687  oddprm  16772  pythagtriplem11  16787  pythagtriplem13  16789  pcpremul  16805  pczndvds2  16829  pc2dvds  16841  pcmpt  16854  smndex1n0mnd  18857  sgrp2nmndlem5  18874  pmtrdifellem4  19427  psgnunilem1  19441  psgnunilem2  19443  efgredlemc  19693  prmcyg  19842  ablfacrplem  20015  ablfac1eulem  20022  ablsimpgfindlem1  20057  islbs2  21035  fidomndrng  21254  frlmssuvc2  21722  1stccnp  23359  fbasfip  23765  metnrmlem1a  24767  xrhmeo  24864  bndth  24877  ioombl1lem4  25483  itg2seq  25665  dvmptdiv  25899  dgrlb  26163  dgrnznn  26174  aaliou2  26268  taylthlem2  26302  taylthlem2OLD  26303  cos02pilt1  26453  dvlog2lem  26579  cxple2  26624  mumullem2  27105  chtub  27138  lgsval2lem  27233  lgsdir  27258  lgsne0  27261  lgsqr  27277  lgseisenlem1  27301  lgseisenlem2  27302  lgseisenlem4  27304  lgsquadlem1  27306  lgsquad2  27312  m1lgs  27314  2sqlem7  27350  2sqblem  27357  nosupbnd1lem1  27634  nosupbnd2  27642  noinfbnd1lem1  27649  noinfbnd2lem1  27656  noinfbnd2  27657  0elold  27828  sltmul2  28064  legso  28396  lmiopp  28599  axlowdimlem6  28751  elntg2  28789  1loopgrvd0  29311  1egrvtxdg0  29318  nfrgr2v  30075  nrt2irr  30276  hmdmadj  31743  strlem1  32053  isoun  32475  archirng  32890  esumrnmpt2  33681  ballotlem4  34112  signswmnd  34183  signslema  34188  bnj1417  34666  satf0n0  34982  fmlaomn0  34994  prv1n  35035  tailfb  35855  unblimceq0  35976  unbdqndv2lem2  35979  topdifinffinlem  36820  icorempo  36824  finxpreclem6  36869  lindsadd  37080  mblfinlem4  37127  3dimlem2  38926  3dimlem3a  38927  3dimlem3OLDN  38929  3dim2  38935  3dim3  38936  lplnnle2at  39008  lplnnlelln  39010  llncvrlpln  39025  lvolnle3at  39049  lvolnlelln  39051  lvolnlelpln  39052  4atlem3  39063  lplncvrlvol  39083  dalem30  39169  dalem35  39174  lhp2at0nle  39502  4atexlemswapqr  39530  ltrncnvel  39609  trlnle  39653  cdleme35sn3a  39926  cdleme46frvlpq  39971  cdlemeg46c  39980  cdlemeg46nlpq  39984  cdleme48gfv  40004  cdlemg7fvbwN  40074  cdlemg4d  40080  cdlemg10a  40107  cdlemg12d  40113  cdlemg27b  40163  cdlemg31d  40167  dihmeetlem6  40776  dochshpsat  40921  dochexmidlem1  40927  mapdindp  41138  lspindp5  41237  dvrelog2b  41531  aks4d1p1p7  41539  aks4d1p6  41546  aks6d1c2p2  41584  aks6d1c5lem1  41601  aks6d1c7lem1  41646  aks6d1c7  41650  metakunt30  41680  xppss12  41711  oexpreposd  41875  dffltz  42052  cmpfiiin  42111  fnwe2lem2  42469  oninfint  42658  dflim5  42752  relexpmulg  43134  relexp01min  43137  relexpxpmin  43141  cvgdvgrat  43744  nelrnmpt  44444  difmap  44574  gtnelioc  44870  ltnelicc  44876  gtnelicc  44879  lenelioc  44915  xrgtnelicc  44917  limciccioolb  45003  limcrecl  45011  limcicciooub  45019  limclner  45033  reclimc  45035  sinaover2ne0  45250  icccncfext  45269  jumpncnp  45280  itgsincmulx  45356  stoweidlem26  45408  stoweidlem35  45417  stirlinglem5  45460  dirker2re  45474  dirkerdenne0  45475  dirkertrigeqlem3  45482  dirkertrigeq  45483  dirkercncflem1  45485  dirkercncflem2  45486  dirkercncflem4  45488  fourierdlem10  45499  fourierdlem24  45513  fourierdlem25  45514  fourierdlem42  45531  fourierdlem44  45533  fourierdlem53  45541  fourierdlem58  45546  fourierdlem62  45550  fourierdlem76  45564  fourierdlem88  45576  fourierdlem104  45592  etransclem41  45657  etransclem44  45660  hoiqssbllem3  46006  smfmbfcex  46142  fsetprcnexALT  46438  ichnreuop  46806  fmtnoinf  46870  lighneallem3  46941  lighneallem4  46944  bits0eALTV  47014  oddprmALTV  47021  0nodd  47226  2nodd  47228  lindslinindsimp1  47519  line2ylem  47818  line2xlem  47820