Theorem mtbird 324

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  2852  eqnbrtrd  5128  rnmptn0  6201  nsuceq0  6405  fvun1  6937  tz7.44-2  8358  oeeulem  8553  onomeneqOLD  9180  supgtoreq  9415  inflb  9434  cantnfp1lem2  9624  cantnflem1  9634  rankxpsuc  9827  cardaleph  10034  cfsuc  10202  cflim2  10208  addnidpi  10846  genpnnp  10950  supaddc  12131  supmul1  12133  nnneneg  12197  indstr2  12861  zbtwnre  12880  xrltnsym  13066  xrlttr  13069  xralrple  13134  supicclub2  13431  flltnz  13726  hashelne0d  14278  hashf1lem1  14365  hashf1lem1OLD  14366  swrdnd  14554  swrd0  14558  sqrtneglem  15163  rlimno1  15550  binomlem  15725  fprodn0f  15885  ruclem12  16134  dvdsle  16203  2tp1odd  16245  smu01lem  16376  rpexp  16609  oddprm  16693  pythagtriplem11  16708  pythagtriplem13  16710  pcpremul  16726  pczndvds2  16750  pc2dvds  16762  pcmpt  16775  smndex1n0mnd  18736  sgrp2nmndlem5  18753  pmtrdifellem4  19275  psgnunilem1  19289  psgnunilem2  19291  efgredlemc  19541  prmcyg  19685  ablfacrplem  19858  ablfac1eulem  19865  ablsimpgfindlem1  19900  islbs2  20674  fidomndrng  20815  frlmssuvc2  21238  1stccnp  22850  fbasfip  23256  metnrmlem1a  24258  xrhmeo  24346  bndth  24358  ioombl1lem4  24962  itg2seq  25144  dvmptdiv  25375  dgrlb  25634  dgrnznn  25645  aaliou2  25737  taylthlem2  25770  cos02pilt1  25919  dvlog2lem  26044  cxple2  26089  mumullem2  26566  chtub  26597  lgsval2lem  26692  lgsdir  26717  lgsne0  26720  lgsqr  26736  lgseisenlem1  26760  lgseisenlem2  26761  lgseisenlem4  26763  lgsquadlem1  26765  lgsquad2  26771  m1lgs  26773  2sqlem7  26809  2sqblem  26816  nosupbnd1lem1  27093  nosupbnd2  27101  noinfbnd1lem1  27108  noinfbnd2lem1  27115  noinfbnd2  27116  legso  27604  lmiopp  27807  axlowdimlem6  27959  elntg2  27997  1loopgrvd0  28515  1egrvtxdg0  28522  nfrgr2v  29279  hmdmadj  30945  strlem1  31255  isoun  31683  archirng  32094  esumrnmpt2  32756  ballotlem4  33187  signswmnd  33258  signslema  33263  bnj1417  33742  satf0n0  34059  fmlaomn0  34071  prv1n  34112  tailfb  34925  unblimceq0  35046  unbdqndv2lem2  35049  topdifinffinlem  35891  icorempo  35895  finxpreclem6  35940  lindsadd  36144  mblfinlem4  36191  3dimlem2  37995  3dimlem3a  37996  3dimlem3OLDN  37998  3dim2  38004  3dim3  38005  lplnnle2at  38077  lplnnlelln  38079  llncvrlpln  38094  lvolnle3at  38118  lvolnlelln  38120  lvolnlelpln  38121  4atlem3  38132  lplncvrlvol  38152  dalem30  38238  dalem35  38243  lhp2at0nle  38571  4atexlemswapqr  38599  ltrncnvel  38678  trlnle  38722  cdleme35sn3a  38995  cdleme46frvlpq  39040  cdlemeg46c  39049  cdlemeg46nlpq  39053  cdleme48gfv  39073  cdlemg7fvbwN  39143  cdlemg4d  39149  cdlemg10a  39176  cdlemg12d  39182  cdlemg27b  39232  cdlemg31d  39236  dihmeetlem6  39845  dochshpsat  39990  dochexmidlem1  39996  mapdindp  40207  lspindp5  40306  dvrelog2b  40596  aks4d1p1p7  40604  aks4d1p6  40611  aks6d1c2p2  40622  metakunt30  40679  xppss12  40723  oexpreposd  40865  dffltz  41030  cmpfiiin  41078  fnwe2lem2  41436  oninfint  41628  dflim5  41722  relexpmulg  42104  relexp01min  42107  relexpxpmin  42111  cvgdvgrat  42715  nelrnmpt  43416  difmap  43549  gtnelioc  43849  ltnelicc  43855  gtnelicc  43858  lenelioc  43894  xrgtnelicc  43896  limciccioolb  43982  limcrecl  43990  limcicciooub  43998  limclner  44012  reclimc  44014  sinaover2ne0  44229  icccncfext  44248  jumpncnp  44259  itgsincmulx  44335  stoweidlem26  44387  stoweidlem35  44396  stirlinglem5  44439  dirker2re  44453  dirkerdenne0  44454  dirkertrigeqlem3  44461  dirkertrigeq  44462  dirkercncflem1  44464  dirkercncflem2  44465  dirkercncflem4  44467  fourierdlem10  44478  fourierdlem24  44492  fourierdlem25  44493  fourierdlem42  44510  fourierdlem44  44512  fourierdlem53  44520  fourierdlem58  44525  fourierdlem62  44529  fourierdlem76  44543  fourierdlem88  44555  fourierdlem104  44571  etransclem41  44636  etransclem44  44639  hoiqssbllem3  44985  smfmbfcex  45121  fsetprcnexALT  45416  ichnreuop  45784  fmtnoinf  45848  lighneallem3  45919  lighneallem4  45922  bits0eALTV  45992  oddprmALTV  45999  0nodd  46224  2nodd  46226  lindslinindsimp1  46658  line2ylem  46957  line2xlem  46959