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  2864  eqnbrtrd  5184  rnmptn0  6275  nsuceq0  6478  fvun1  7013  tz7.44-2  8463  oeeulem  8657  onomeneqOLD  9292  supgtoreq  9539  inflb  9558  cantnfp1lem2  9748  cantnflem1  9758  rankxpsuc  9951  cardaleph  10158  cfsuc  10326  cflim2  10332  addnidpi  10970  genpnnp  11074  supaddc  12262  supmul1  12264  nnneneg  12328  indstr2  12992  zbtwnre  13011  xrltnsym  13199  xrlttr  13202  xralrple  13267  supicclub2  13564  flltnz  13862  hashelne0d  14417  hashf1lem1  14504  swrdnd  14702  swrd0  14706  sqrtneglem  15315  rlimno1  15702  binomlem  15877  fprodn0f  16039  ruclem12  16289  dvdsle  16358  2tp1odd  16400  smu01lem  16531  rpexp  16769  oddprm  16857  pythagtriplem11  16872  pythagtriplem13  16874  pcpremul  16890  pczndvds2  16914  pc2dvds  16926  pcmpt  16939  smndex1n0mnd  18947  sgrp2nmndlem5  18964  pmtrdifellem4  19521  psgnunilem1  19535  psgnunilem2  19537  efgredlemc  19787  prmcyg  19936  ablfacrplem  20109  ablfac1eulem  20116  ablsimpgfindlem1  20151  fidomndrng  20796  islbs2  21179  frlmssuvc2  21838  1stccnp  23491  fbasfip  23897  metnrmlem1a  24899  xrhmeo  24996  bndth  25009  ioombl1lem4  25615  itg2seq  25797  dvmptdiv  26032  dgrlb  26295  dgrnznn  26306  aaliou2  26400  taylthlem2  26434  taylthlem2OLD  26435  cos02pilt1  26586  dvlog2lem  26712  cxple2  26757  mumullem2  27241  chtub  27274  lgsval2lem  27369  lgsdir  27394  lgsne0  27397  lgsqr  27413  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem4  27440  lgsquadlem1  27442  lgsquad2  27448  m1lgs  27450  2sqlem7  27486  2sqblem  27493  nosupbnd1lem1  27771  nosupbnd2  27779  noinfbnd1lem1  27786  noinfbnd2lem1  27793  noinfbnd2  27794  0elold  27965  sltmul2  28215  legso  28625  lmiopp  28828  axlowdimlem6  28980  elntg2  29018  1loopgrvd0  29540  1egrvtxdg0  29547  nfrgr2v  30304  nrt2irr  30505  hmdmadj  31972  strlem1  32282  isoun  32713  expgt0b  32820  archirng  33168  rsprprmprmidl  33515  rprmdvdsprod  33527  esumrnmpt2  34032  ballotlem4  34463  signswmnd  34534  signslema  34539  bnj1417  35017  satf0n0  35346  fmlaomn0  35358  prv1n  35399  tailfb  36343  weiunfr  36433  unblimceq0  36473  unbdqndv2lem2  36476  topdifinffinlem  37313  icorempo  37317  finxpreclem6  37362  lindsadd  37573  mblfinlem4  37620  3dimlem2  39416  3dimlem3a  39417  3dimlem3OLDN  39419  3dim2  39425  3dim3  39426  lplnnle2at  39498  lplnnlelln  39500  llncvrlpln  39515  lvolnle3at  39539  lvolnlelln  39541  lvolnlelpln  39542  4atlem3  39553  lplncvrlvol  39573  dalem30  39659  dalem35  39664  lhp2at0nle  39992  4atexlemswapqr  40020  ltrncnvel  40099  trlnle  40143  cdleme35sn3a  40416  cdleme46frvlpq  40461  cdlemeg46c  40470  cdlemeg46nlpq  40474  cdleme48gfv  40494  cdlemg7fvbwN  40564  cdlemg4d  40570  cdlemg10a  40597  cdlemg12d  40603  cdlemg27b  40653  cdlemg31d  40657  dihmeetlem6  41266  dochshpsat  41411  dochexmidlem1  41417  mapdindp  41628  lspindp5  41727  dvrelog2b  42023  aks4d1p1p7  42031  aks4d1p6  42038  aks6d1c2p2  42076  aks6d1c5lem1  42093  aks6d1c7lem1  42137  aks6d1c7  42141  metakunt30  42191  xppss12  42222  oexpreposd  42309  dffltz  42589  cmpfiiin  42653  fnwe2lem2  43008  oninfint  43197  dflim5  43291  relexpmulg  43672  relexp01min  43675  relexpxpmin  43679  cvgdvgrat  44282  nelrnmpt  44986  difmap  45114  gtnelioc  45409  ltnelicc  45415  gtnelicc  45418  lenelioc  45454  xrgtnelicc  45456  limciccioolb  45542  limcrecl  45550  limcicciooub  45558  limclner  45572  reclimc  45574  sinaover2ne0  45789  icccncfext  45808  jumpncnp  45819  itgsincmulx  45895  stoweidlem26  45947  stoweidlem35  45956  stirlinglem5  45999  dirker2re  46013  dirkerdenne0  46014  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncflem1  46024  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem10  46038  fourierdlem24  46052  fourierdlem25  46053  fourierdlem42  46070  fourierdlem44  46072  fourierdlem53  46080  fourierdlem58  46085  fourierdlem62  46089  fourierdlem76  46103  fourierdlem88  46115  fourierdlem104  46131  etransclem41  46196  etransclem44  46199  hoiqssbllem3  46545  smfmbfcex  46681  fsetprcnexALT  46977  ichnreuop  47346  fmtnoinf  47410  lighneallem3  47481  lighneallem4  47484  bits0eALTV  47554  oddprmALTV  47561  0nodd  47893  2nodd  47895  lindslinindsimp1  48186  line2ylem  48485  line2xlem  48487