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  2851  eqnbrtrd  5109  rnmptn0  6191  nsuceq0  6391  fvun1  6913  tz7.44-2  8326  oeeulem  8516  supgtoreq  9355  inflb  9374  cantnfp1lem2  9569  cantnflem1  9579  rankxpsuc  9772  cardaleph  9977  cfsuc  10145  cflim2  10151  addnidpi  10789  genpnnp  10893  supaddc  12086  supmul1  12088  nnneneg  12157  indstr2  12822  zbtwnre  12841  xrltnsym  13033  xrlttr  13036  xralrple  13101  supicclub2  13401  flltnz  13712  hashelne0d  14272  hashf1lem1  14359  swrdnd  14559  swrd0  14563  sqrtneglem  15170  rlimno1  15558  binomlem  15733  fprodn0f  15895  ruclem12  16147  dvdsle  16218  2tp1odd  16260  smu01lem  16393  rpexp  16630  oddprm  16719  pythagtriplem11  16734  pythagtriplem13  16736  pcpremul  16752  pczndvds2  16776  pc2dvds  16788  pcmpt  16801  smndex1n0mnd  18817  sgrp2nmndlem5  18834  pmtrdifellem4  19389  psgnunilem1  19403  psgnunilem2  19405  efgredlemc  19655  prmcyg  19804  ablfacrplem  19977  ablfac1eulem  19984  ablsimpgfindlem1  20019  fidomndrng  20686  islbs2  21089  frlmssuvc2  21730  1stccnp  23375  fbasfip  23781  metnrmlem1a  24772  xrhmeo  24869  bndth  24882  ioombl1lem4  25487  itg2seq  25668  dvmptdiv  25903  dgrlb  26166  dgrnznn  26177  aaliou2  26273  taylthlem2  26307  taylthlem2OLD  26308  cos02pilt1  26460  dvlog2lem  26586  cxple2  26631  mumullem2  27115  chtub  27148  lgsval2lem  27243  lgsdir  27268  lgsne0  27271  lgsqr  27287  lgseisenlem1  27311  lgseisenlem2  27312  lgseisenlem4  27314  lgsquadlem1  27316  lgsquad2  27322  m1lgs  27324  2sqlem7  27360  2sqblem  27367  nosupbnd1lem1  27645  nosupbnd2  27653  noinfbnd1lem1  27660  noinfbnd2lem1  27667  noinfbnd2  27668  0elold  27853  sltmul2  28108  pw2cut2  28380  legso  28575  lmiopp  28778  axlowdimlem6  28923  elntg2  28961  1loopgrvd0  29481  1egrvtxdg0  29488  nfrgr2v  30247  nrt2irr  30448  hmdmadj  31915  strlem1  32225  isoun  32678  expgt0b  32794  archirng  33152  rsprprmprmidl  33482  rprmdvdsprod  33494  extdgfialglem1  33700  constrcon  33782  esumrnmpt2  34076  ballotlem4  34507  signswmnd  34565  signslema  34570  bnj1417  35048  satf0n0  35410  fmlaomn0  35422  prv1n  35463  tailfb  36410  weiunfr  36500  unblimceq0  36540  unbdqndv2lem2  36543  topdifinffinlem  37380  icorempo  37384  finxpreclem6  37429  lindsadd  37652  mblfinlem4  37699  3dimlem2  39497  3dimlem3a  39498  3dimlem3OLDN  39500  3dim2  39506  3dim3  39507  lplnnle2at  39579  lplnnlelln  39581  llncvrlpln  39596  lvolnle3at  39620  lvolnlelln  39622  lvolnlelpln  39623  4atlem3  39634  lplncvrlvol  39654  dalem30  39740  dalem35  39745  lhp2at0nle  40073  4atexlemswapqr  40101  ltrncnvel  40180  trlnle  40224  cdleme35sn3a  40497  cdleme46frvlpq  40542  cdlemeg46c  40551  cdlemeg46nlpq  40555  cdleme48gfv  40575  cdlemg7fvbwN  40645  cdlemg4d  40651  cdlemg10a  40678  cdlemg12d  40684  cdlemg27b  40734  cdlemg31d  40738  dihmeetlem6  41347  dochshpsat  41492  dochexmidlem1  41498  mapdindp  41709  lspindp5  41808  dvrelog2b  42098  aks4d1p1p7  42106  aks4d1p6  42113  aks6d1c2p2  42151  aks6d1c5lem1  42168  aks6d1c7lem1  42212  aks6d1c7  42216  xppss12  42261  oexpreposd  42354  mulltgt0d  42514  mullt0b2d  42516  sn-mullt0d  42517  dffltz  42666  cmpfiiin  42729  fnwe2lem2  43083  oninfint  43268  dflim5  43361  relexpmulg  43742  relexp01min  43745  relexpxpmin  43749  cvgdvgrat  44345  nelrnmpt  45120  difmap  45243  gtnelioc  45530  ltnelicc  45536  gtnelicc  45539  lenelioc  45575  xrgtnelicc  45577  limciccioolb  45660  limcrecl  45668  limcicciooub  45674  limclner  45688  reclimc  45690  sinaover2ne0  45905  icccncfext  45924  jumpncnp  45935  itgsincmulx  46011  stoweidlem26  46063  stoweidlem35  46072  stirlinglem5  46115  dirker2re  46129  dirkerdenne0  46130  dirkertrigeqlem3  46137  dirkertrigeq  46138  dirkercncflem1  46140  dirkercncflem2  46141  dirkercncflem4  46143  fourierdlem10  46154  fourierdlem24  46168  fourierdlem25  46169  fourierdlem42  46186  fourierdlem44  46188  fourierdlem53  46196  fourierdlem58  46201  fourierdlem62  46205  fourierdlem76  46219  fourierdlem88  46231  fourierdlem104  46247  etransclem41  46312  etransclem44  46315  hoiqssbllem3  46661  smfmbfcex  46797  fsetprcnexALT  47092  difltmodne  47372  minusmodnep2tmod  47383  modm1p1ne  47400  ichnreuop  47502  fmtnoinf  47566  lighneallem3  47637  lighneallem4  47640  bits0eALTV  47710  oddprmALTV  47717  upgrimpths  47939  gpg5nbgrvtx03starlem1  48098  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx03starlem3  48100  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem2  48102  gpg5nbgrvtx13starlem3  48103  gpg3kgrtriexlem5  48117  gpg5edgnedg  48160  0nodd  48200  2nodd  48202  lindslinindsimp1  48488  line2ylem  48782  line2xlem  48784