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  2854  eqnbrtrd  5137  rnmptn0  6233  nsuceq0  6436  fvun1  6969  tz7.44-2  8419  oeeulem  8611  onomeneqOLD  9236  supgtoreq  9481  inflb  9500  cantnfp1lem2  9691  cantnflem1  9701  rankxpsuc  9894  cardaleph  10101  cfsuc  10269  cflim2  10275  addnidpi  10913  genpnnp  11017  supaddc  12207  supmul1  12209  nnneneg  12273  indstr2  12941  zbtwnre  12960  xrltnsym  13151  xrlttr  13154  xralrple  13219  supicclub2  13519  flltnz  13826  hashelne0d  14384  hashf1lem1  14471  swrdnd  14670  swrd0  14674  sqrtneglem  15283  rlimno1  15668  binomlem  15843  fprodn0f  16005  ruclem12  16257  dvdsle  16327  2tp1odd  16369  smu01lem  16502  rpexp  16739  oddprm  16828  pythagtriplem11  16843  pythagtriplem13  16845  pcpremul  16861  pczndvds2  16885  pc2dvds  16897  pcmpt  16910  smndex1n0mnd  18888  sgrp2nmndlem5  18905  pmtrdifellem4  19458  psgnunilem1  19472  psgnunilem2  19474  efgredlemc  19724  prmcyg  19873  ablfacrplem  20046  ablfac1eulem  20053  ablsimpgfindlem1  20088  fidomndrng  20731  islbs2  21113  frlmssuvc2  21753  1stccnp  23398  fbasfip  23804  metnrmlem1a  24796  xrhmeo  24893  bndth  24906  ioombl1lem4  25512  itg2seq  25693  dvmptdiv  25928  dgrlb  26191  dgrnznn  26202  aaliou2  26298  taylthlem2  26332  taylthlem2OLD  26333  cos02pilt1  26485  dvlog2lem  26611  cxple2  26656  mumullem2  27140  chtub  27173  lgsval2lem  27268  lgsdir  27293  lgsne0  27296  lgsqr  27312  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem4  27339  lgsquadlem1  27341  lgsquad2  27347  m1lgs  27349  2sqlem7  27385  2sqblem  27392  nosupbnd1lem1  27670  nosupbnd2  27678  noinfbnd1lem1  27685  noinfbnd2lem1  27692  noinfbnd2  27693  0elold  27864  sltmul2  28114  legso  28524  lmiopp  28727  axlowdimlem6  28872  elntg2  28910  1loopgrvd0  29430  1egrvtxdg0  29437  nfrgr2v  30199  nrt2irr  30400  hmdmadj  31867  strlem1  32177  isoun  32625  expgt0b  32741  archirng  33132  rsprprmprmidl  33483  rprmdvdsprod  33495  constrcon  33754  esumrnmpt2  34045  ballotlem4  34477  signswmnd  34535  signslema  34540  bnj1417  35018  satf0n0  35346  fmlaomn0  35358  prv1n  35399  tailfb  36341  weiunfr  36431  unblimceq0  36471  unbdqndv2lem2  36474  topdifinffinlem  37311  icorempo  37315  finxpreclem6  37360  lindsadd  37583  mblfinlem4  37630  3dimlem2  39424  3dimlem3a  39425  3dimlem3OLDN  39427  3dim2  39433  3dim3  39434  lplnnle2at  39506  lplnnlelln  39508  llncvrlpln  39523  lvolnle3at  39547  lvolnlelln  39549  lvolnlelpln  39550  4atlem3  39561  lplncvrlvol  39581  dalem30  39667  dalem35  39672  lhp2at0nle  40000  4atexlemswapqr  40028  ltrncnvel  40107  trlnle  40151  cdleme35sn3a  40424  cdleme46frvlpq  40469  cdlemeg46c  40478  cdlemeg46nlpq  40482  cdleme48gfv  40502  cdlemg7fvbwN  40572  cdlemg4d  40578  cdlemg10a  40605  cdlemg12d  40611  cdlemg27b  40661  cdlemg31d  40665  dihmeetlem6  41274  dochshpsat  41419  dochexmidlem1  41425  mapdindp  41636  lspindp5  41735  dvrelog2b  42025  aks4d1p1p7  42033  aks4d1p6  42040  aks6d1c2p2  42078  aks6d1c5lem1  42095  aks6d1c7lem1  42139  aks6d1c7  42143  metakunt30  42193  xppss12  42226  oexpreposd  42318  dffltz  42604  cmpfiiin  42667  fnwe2lem2  43022  oninfint  43207  dflim5  43300  relexpmulg  43681  relexp01min  43684  relexpxpmin  43688  cvgdvgrat  44285  nelrnmpt  45056  difmap  45179  gtnelioc  45468  ltnelicc  45474  gtnelicc  45477  lenelioc  45513  xrgtnelicc  45515  limciccioolb  45598  limcrecl  45606  limcicciooub  45614  limclner  45628  reclimc  45630  sinaover2ne0  45845  icccncfext  45864  jumpncnp  45875  itgsincmulx  45951  stoweidlem26  46003  stoweidlem35  46012  stirlinglem5  46055  dirker2re  46069  dirkerdenne0  46070  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem1  46080  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem10  46094  fourierdlem24  46108  fourierdlem25  46109  fourierdlem42  46126  fourierdlem44  46128  fourierdlem53  46136  fourierdlem58  46141  fourierdlem62  46145  fourierdlem76  46159  fourierdlem88  46171  fourierdlem104  46187  etransclem41  46252  etransclem44  46255  hoiqssbllem3  46601  smfmbfcex  46737  fsetprcnexALT  47039  difltmodne  47319  minusmodnep2tmod  47330  ichnreuop  47434  fmtnoinf  47498  lighneallem3  47569  lighneallem4  47572  bits0eALTV  47642  oddprmALTV  47649  upgrimpths  47870  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  gpg3kgrtriexlem5  48037  0nodd  48093  2nodd  48095  lindslinindsimp1  48381  line2ylem  48679  line2xlem  48681