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  2858  eqnbrtrd  5094  rnmptn0  6149  nsuceq0  6348  fvun1  6861  tz7.44-2  8236  oeeulem  8430  onomeneqOLD  9010  supgtoreq  9227  inflb  9246  cantnfp1lem2  9435  cantnflem1  9445  rankxpsuc  9638  cardaleph  9843  cfsuc  10011  cflim2  10017  addnidpi  10655  genpnnp  10759  supaddc  11940  supmul1  11942  nnneneg  12006  indstr2  12665  zbtwnre  12684  xrltnsym  12869  xrlttr  12872  xralrple  12937  supicclub2  13234  flltnz  13529  hashelne0d  14081  hashf1lem1  14166  hashf1lem1OLD  14167  swrdnd  14365  swrd0  14369  sqrtneglem  14976  rlimno1  15363  binomlem  15539  fprodn0f  15699  ruclem12  15948  dvdsle  16017  2tp1odd  16059  smu01lem  16190  rpexp  16425  oddprm  16509  pythagtriplem11  16524  pythagtriplem13  16526  pcpremul  16542  pczndvds2  16566  pc2dvds  16578  pcmpt  16591  smndex1n0mnd  18549  sgrp2nmndlem5  18566  pmtrdifellem4  19085  psgnunilem1  19099  psgnunilem2  19101  efgredlemc  19349  prmcyg  19493  ablfacrplem  19666  ablfac1eulem  19673  ablsimpgfindlem1  19708  islbs2  20414  fidomndrng  20577  frlmssuvc2  21000  1stccnp  22611  fbasfip  23017  metnrmlem1a  24019  xrhmeo  24107  bndth  24119  ioombl1lem4  24723  itg2seq  24905  dvmptdiv  25136  dgrlb  25395  dgrnznn  25406  aaliou2  25498  taylthlem2  25531  cos02pilt1  25680  dvlog2lem  25805  cxple2  25850  mumullem2  26327  chtub  26358  lgsval2lem  26453  lgsdir  26478  lgsne0  26481  lgsqr  26497  lgseisenlem1  26521  lgseisenlem2  26522  lgseisenlem4  26524  lgsquadlem1  26526  lgsquad2  26532  m1lgs  26534  2sqlem7  26570  2sqblem  26577  legso  26958  lmiopp  27161  axlowdimlem6  27313  elntg2  27351  1loopgrvd0  27869  1egrvtxdg0  27876  nfrgr2v  28633  hmdmadj  30299  strlem1  30609  isoun  31031  archirng  31439  esumrnmpt2  32033  ballotlem4  32462  signswmnd  32533  signslema  32538  bnj1417  33018  satf0n0  33337  fmlaomn0  33349  prv1n  33390  nosupbnd1lem1  33908  nosupbnd2  33916  noinfbnd1lem1  33923  noinfbnd2lem1  33930  noinfbnd2  33931  tailfb  34563  unblimceq0  34684  unbdqndv2lem2  34687  topdifinffinlem  35515  icorempo  35519  finxpreclem6  35564  lindsadd  35767  mblfinlem4  35814  3dimlem2  37470  3dimlem3a  37471  3dimlem3OLDN  37473  3dim2  37479  3dim3  37480  lplnnle2at  37552  lplnnlelln  37554  llncvrlpln  37569  lvolnle3at  37593  lvolnlelln  37595  lvolnlelpln  37596  4atlem3  37607  lplncvrlvol  37627  dalem30  37713  dalem35  37718  lhp2at0nle  38046  4atexlemswapqr  38074  ltrncnvel  38153  trlnle  38197  cdleme35sn3a  38470  cdleme46frvlpq  38515  cdlemeg46c  38524  cdlemeg46nlpq  38528  cdleme48gfv  38548  cdlemg7fvbwN  38618  cdlemg4d  38624  cdlemg10a  38651  cdlemg12d  38657  cdlemg27b  38707  cdlemg31d  38711  dihmeetlem6  39320  dochshpsat  39465  dochexmidlem1  39471  mapdindp  39682  lspindp5  39781  dvrelog2b  40071  aks4d1p1p7  40079  aks4d1p6  40086  metakunt30  40151  xppss12  40201  oexpreposd  40318  dffltz  40468  cmpfiiin  40516  fnwe2lem2  40873  relexpmulg  41288  relexp01min  41291  relexpxpmin  41295  cvgdvgrat  41901  nelrnmpt  42604  difmap  42717  gtnelioc  42999  ltnelicc  43005  gtnelicc  43008  lenelioc  43044  xrgtnelicc  43046  limciccioolb  43132  limcrecl  43140  limcicciooub  43148  limclner  43162  reclimc  43164  sinaover2ne0  43379  icccncfext  43398  jumpncnp  43409  itgsincmulx  43485  stoweidlem26  43537  stoweidlem35  43546  stirlinglem5  43589  dirker2re  43603  dirkerdenne0  43604  dirkertrigeqlem3  43611  dirkertrigeq  43612  dirkercncflem1  43614  dirkercncflem2  43615  dirkercncflem4  43617  fourierdlem10  43628  fourierdlem24  43642  fourierdlem25  43643  fourierdlem42  43660  fourierdlem44  43662  fourierdlem53  43670  fourierdlem58  43675  fourierdlem62  43679  fourierdlem76  43693  fourierdlem88  43705  fourierdlem104  43721  etransclem41  43786  etransclem44  43789  hoiqssbllem3  44132  smfmbfcex  44262  fsetprcnexALT  44523  ichnreuop  44891  fmtnoinf  44955  lighneallem3  45026  lighneallem4  45029  bits0eALTV  45099  oddprmALTV  45106  0nodd  45331  2nodd  45333  lindslinindsimp1  45765  line2ylem  46064  line2xlem  46066