Theorem mtbird 328

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 232	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 201	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  eqneltrd  2886  eqnbrtrd  5134  nelrnmpt  5962  rnmptn0  6250  nsuceq0  6453  fvun1  6979  tz7.44-2  8403  oeeulem  8596  supgtoreq  9441  inflb  9460  cantnfp1lem2  9658  cantnflem1  9668  rankxpsuc  9864  cardaleph  10092  cfsuc  10259  cflim2  10265  addnidpi  10904  genpnnp  11008  supaddc  12200  supmul1  12202  nnneneg  12289  indstr2  12969  zbtwnre  12988  xrltnsym  13180  xrlttr  13183  xralrple  13249  supicclub2  13549  flltnz  13864  hashelne0d  14424  hashf1lem1  14512  swrdnd  14716  swrd0  14720  sqrtneglem  15343  rlimno1  15731  binomlem  15909  fprodn0f  16071  ruclem12  16322  dvdsle  16393  2tp1odd  16435  smu01lem  16568  rpexp  16806  oddprm  16895  pythagtriplem11  16910  pythagtriplem13  16912  pcpremul  16928  pczndvds2  16952  pc2dvds  16964  pcmpt  16977  smndex1n0mnd  19005  sgrp2nmndlem5  19022  pmtrdifellem4  19580  psgnunilem1  19594  psgnunilem2  19596  efgredlemc  19846  prmcyg  19995  ablfacrplem  20168  ablfac1eulem  20175  ablsimpgfindlem1  20210  fidomndrng  20914  islbs2  21315  frlmssuvc2  21982  1stccnp  23656  fbasfip  24062  metnrmlem1a  25053  xrhmeo  25142  bndth  25154  ioombl1lem4  25757  itg2seq  25938  dvmptdiv  26170  dgrlb  26430  dgrnznn  26441  aaliou2  26540  taylthlem2  26574  cos02pilt1  26728  dvlog2lem  26854  cxple2  26899  mumullem2  27381  chtub  27413  lgsval2lem  27508  lgsdir  27533  lgsne0  27536  lgsqr  27552  lgseisenlem1  27576  lgseisenlem2  27577  lgseisenlem4  27579  lgsquadlem1  27581  lgsquad2  27587  m1lgs  27589  2sqlem7  27625  2sqblem  27632  nosupbnd1lem1  27909  nosupbnd2  27917  noinfbnd1lem1  27924  noinfbnd2lem1  27931  noinfbnd2  27932  0elold  28140  ltmuls2  28401  pw2cut2  28692  legso  28905  tgelrnpln  29095  plngrotlem2  29107  lmiopp  29149  axlowdimlem6  29334  elntg2  29372  1loopgrvd0  29891  1egrvtxdg0  29898  nfrgr2v  30660  nrt2irr  30861  hmdmadj  32329  strlem1  32639  isoun  33084  expgt0b  33198  archirng  33539  rsprprmprmidl  33843  rprmdvdsprod  33855  extdgfialglem1  34113  constrcon  34195  esumrnmpt2  34489  ballotlem4  34920  signswmnd  34975  signslema  34980  bnj1417  35460  satf0n0  35890  fmlaomn0  35902  prv1n  35943  tailfb  36928  weiunfr  37018  unblimceq0  37136  unbdqndv2lem2  37139  qdiff  38011  topdifinffinlem  38033  icorempo  38037  finxpreclem6  38082  lindsadd  38304  mblfinlem4  38351  3dimlem2  40273  3dimlem3a  40274  3dimlem3OLDN  40276  3dim2  40282  3dim3  40283  lplnnle2at  40355  lplnnlelln  40357  llncvrlpln  40372  lvolnle3at  40396  lvolnlelln  40398  lvolnlelpln  40399  4atlem3  40410  lplncvrlvol  40430  dalem30  40516  dalem35  40521  lhp2at0nle  40849  4atexlemswapqr  40877  ltrncnvel  40956  trlnle  41000  cdleme35sn3a  41273  cdleme46frvlpq  41318  cdlemeg46c  41327  cdlemeg46nlpq  41331  cdleme48gfv  41351  cdlemg7fvbwN  41421  cdlemg4d  41427  cdlemg10a  41454  cdlemg12d  41460  cdlemg27b  41510  cdlemg31d  41514  dihmeetlem6  42123  dochshpsat  42268  dochexmidlem1  42274  mapdindp  42485  lspindp5  42584  dvrelog2b  42873  aks4d1p1p7  42881  aks4d1p6  42888  aks6d1c2p2  42926  aks6d1c5lem1  42943  aks6d1c7lem1  42987  aks6d1c7  42991  xppss12  43040  oexpreposd  43123  mulltgt0d  43296  mullt0b2d  43298  sn-mullt0d  43299  dffltz  43406  cmpfiiin  43468  fnwe2lem2  43818  oninfint  44003  dflim5  44096  relexpmulg  44476  relexp01min  44479  relexpxpmin  44483  cvgdvgrat  45063  difmap  45963  gtnelioc  46247  ltnelicc  46253  gtnelicc  46256  lenelioc  46292  xrgtnelicc  46294  limciccioolb  46377  limcrecl  46385  limcicciooub  46391  limclner  46405  reclimc  46407  sinaover2ne0  46622  icccncfext  46641  jumpncnp  46652  itgsincmulx  46728  stoweidlem26  46780  stoweidlem35  46789  stirlinglem5  46832  dirker2re  46846  dirkerdenne0  46847  dirkertrigeqlem3  46854  dirkertrigeq  46855  dirkercncflem1  46857  dirkercncflem2  46858  dirkercncflem4  46860  fourierdlem10  46871  fourierdlem24  46885  fourierdlem25  46886  fourierdlem42  46903  fourierdlem44  46905  fourierdlem53  46913  fourierdlem58  46918  fourierdlem62  46922  fourierdlem76  46936  fourierdlem88  46948  fourierdlem104  46964  etransclem41  47029  etransclem44  47032  hoiqssbllem3  47378  smfmbfcex  47514  fsetprcnexALT  47839  difltmodne  48125  minusmodnep2tmod  48136  modm1p1ne  48153  ichnreuop  48261  fmtnoinf  48328  lighneallem3  48399  lighneallem4  48402  bits0eALTV  48485  oddprmALTV  48492  upgrimpths  48714  gpg5nbgrvtx03starlem1  48873  gpg5nbgrvtx03starlem2  48874  gpg5nbgrvtx03starlem3  48875  gpg5nbgrvtx13starlem1  48876  gpg5nbgrvtx13starlem2  48877  gpg5nbgrvtx13starlem3  48878  gpg3kgrtriexlem5  48892  gpg5edgnedg  48935  0nodd  48975  2nodd  48977  smprngprmrng  49144  lindslinindsimp1  49277  line2ylem  49571  line2xlem  49573