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  2853  eqnbrtrd  5111  rnmptn0  6196  nsuceq0  6396  fvun1  6919  tz7.44-2  8332  oeeulem  8522  supgtoreq  9362  inflb  9381  cantnfp1lem2  9576  cantnflem1  9586  rankxpsuc  9782  cardaleph  9987  cfsuc  10155  cflim2  10161  addnidpi  10799  genpnnp  10903  supaddc  12096  supmul1  12098  nnneneg  12167  indstr2  12827  zbtwnre  12846  xrltnsym  13038  xrlttr  13041  xralrple  13106  supicclub2  13406  flltnz  13717  hashelne0d  14277  hashf1lem1  14364  swrdnd  14564  swrd0  14568  sqrtneglem  15175  rlimno1  15563  binomlem  15738  fprodn0f  15900  ruclem12  16152  dvdsle  16223  2tp1odd  16265  smu01lem  16398  rpexp  16635  oddprm  16724  pythagtriplem11  16739  pythagtriplem13  16741  pcpremul  16757  pczndvds2  16781  pc2dvds  16793  pcmpt  16806  smndex1n0mnd  18822  sgrp2nmndlem5  18839  pmtrdifellem4  19393  psgnunilem1  19407  psgnunilem2  19409  efgredlemc  19659  prmcyg  19808  ablfacrplem  19981  ablfac1eulem  19988  ablsimpgfindlem1  20023  fidomndrng  20690  islbs2  21093  frlmssuvc2  21734  1stccnp  23378  fbasfip  23784  metnrmlem1a  24775  xrhmeo  24872  bndth  24885  ioombl1lem4  25490  itg2seq  25671  dvmptdiv  25906  dgrlb  26169  dgrnznn  26180  aaliou2  26276  taylthlem2  26310  taylthlem2OLD  26311  cos02pilt1  26463  dvlog2lem  26589  cxple2  26634  mumullem2  27118  chtub  27151  lgsval2lem  27246  lgsdir  27271  lgsne0  27274  lgsqr  27290  lgseisenlem1  27314  lgseisenlem2  27315  lgseisenlem4  27317  lgsquadlem1  27319  lgsquad2  27325  m1lgs  27327  2sqlem7  27363  2sqblem  27370  nosupbnd1lem1  27648  nosupbnd2  27656  noinfbnd1lem1  27663  noinfbnd2lem1  27670  noinfbnd2  27671  0elold  27856  sltmul2  28111  pw2cut2  28383  legso  28578  lmiopp  28781  axlowdimlem6  28927  elntg2  28965  1loopgrvd0  29485  1egrvtxdg0  29492  nfrgr2v  30254  nrt2irr  30455  hmdmadj  31922  strlem1  32232  isoun  32687  expgt0b  32804  archirng  33164  rsprprmprmidl  33494  rprmdvdsprod  33506  extdgfialglem1  33726  constrcon  33808  esumrnmpt2  34102  ballotlem4  34533  signswmnd  34591  signslema  34596  bnj1417  35074  satf0n0  35443  fmlaomn0  35455  prv1n  35496  tailfb  36442  weiunfr  36532  unblimceq0  36572  unbdqndv2lem2  36575  topdifinffinlem  37412  icorempo  37416  finxpreclem6  37461  lindsadd  37673  mblfinlem4  37720  3dimlem2  39578  3dimlem3a  39579  3dimlem3OLDN  39581  3dim2  39587  3dim3  39588  lplnnle2at  39660  lplnnlelln  39662  llncvrlpln  39677  lvolnle3at  39701  lvolnlelln  39703  lvolnlelpln  39704  4atlem3  39715  lplncvrlvol  39735  dalem30  39821  dalem35  39826  lhp2at0nle  40154  4atexlemswapqr  40182  ltrncnvel  40261  trlnle  40305  cdleme35sn3a  40578  cdleme46frvlpq  40623  cdlemeg46c  40632  cdlemeg46nlpq  40636  cdleme48gfv  40656  cdlemg7fvbwN  40726  cdlemg4d  40732  cdlemg10a  40759  cdlemg12d  40765  cdlemg27b  40815  cdlemg31d  40819  dihmeetlem6  41428  dochshpsat  41573  dochexmidlem1  41579  mapdindp  41790  lspindp5  41889  dvrelog2b  42179  aks4d1p1p7  42187  aks4d1p6  42194  aks6d1c2p2  42232  aks6d1c5lem1  42249  aks6d1c7lem1  42293  aks6d1c7  42297  xppss12  42347  oexpreposd  42440  mulltgt0d  42600  mullt0b2d  42602  sn-mullt0d  42603  dffltz  42752  cmpfiiin  42814  fnwe2lem2  43168  oninfint  43353  dflim5  43446  relexpmulg  43827  relexp01min  43830  relexpxpmin  43834  cvgdvgrat  44430  nelrnmpt  45205  difmap  45328  gtnelioc  45615  ltnelicc  45621  gtnelicc  45624  lenelioc  45660  xrgtnelicc  45662  limciccioolb  45745  limcrecl  45753  limcicciooub  45759  limclner  45773  reclimc  45775  sinaover2ne0  45990  icccncfext  46009  jumpncnp  46020  itgsincmulx  46096  stoweidlem26  46148  stoweidlem35  46157  stirlinglem5  46200  dirker2re  46214  dirkerdenne0  46215  dirkertrigeqlem3  46222  dirkertrigeq  46223  dirkercncflem1  46225  dirkercncflem2  46226  dirkercncflem4  46228  fourierdlem10  46239  fourierdlem24  46253  fourierdlem25  46254  fourierdlem42  46271  fourierdlem44  46273  fourierdlem53  46281  fourierdlem58  46286  fourierdlem62  46290  fourierdlem76  46304  fourierdlem88  46316  fourierdlem104  46332  etransclem41  46397  etransclem44  46400  hoiqssbllem3  46746  smfmbfcex  46882  fsetprcnexALT  47186  difltmodne  47466  minusmodnep2tmod  47477  modm1p1ne  47494  ichnreuop  47596  fmtnoinf  47660  lighneallem3  47731  lighneallem4  47734  bits0eALTV  47804  oddprmALTV  47811  upgrimpths  48033  gpg5nbgrvtx03starlem1  48192  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx03starlem3  48194  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem2  48196  gpg5nbgrvtx13starlem3  48197  gpg3kgrtriexlem5  48211  gpg5edgnedg  48254  0nodd  48294  2nodd  48296  lindslinindsimp1  48582  line2ylem  48876  line2xlem  48878