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  2856  eqnbrtrd  5103  nelrnmpt  5922  rnmptn0  6208  nsuceq0  6408  fvun1  6931  tz7.44-2  8346  oeeulem  8537  supgtoreq  9384  inflb  9403  cantnfp1lem2  9600  cantnflem1  9610  rankxpsuc  9806  cardaleph  10011  cfsuc  10179  cflim2  10185  addnidpi  10824  genpnnp  10928  supaddc  12123  supmul1  12125  nnneneg  12212  indstr2  12877  zbtwnre  12896  xrltnsym  13088  xrlttr  13091  xralrple  13157  supicclub2  13457  flltnz  13770  hashelne0d  14330  hashf1lem1  14417  swrdnd  14617  swrd0  14621  sqrtneglem  15228  rlimno1  15616  binomlem  15794  fprodn0f  15956  ruclem12  16208  dvdsle  16279  2tp1odd  16321  smu01lem  16454  rpexp  16692  oddprm  16781  pythagtriplem11  16796  pythagtriplem13  16798  pcpremul  16814  pczndvds2  16838  pc2dvds  16850  pcmpt  16863  smndex1n0mnd  18883  sgrp2nmndlem5  18900  pmtrdifellem4  19454  psgnunilem1  19468  psgnunilem2  19470  efgredlemc  19720  prmcyg  19869  ablfacrplem  20042  ablfac1eulem  20049  ablsimpgfindlem1  20084  fidomndrng  20750  islbs2  21152  frlmssuvc2  21775  1stccnp  23427  fbasfip  23833  metnrmlem1a  24824  xrhmeo  24913  bndth  24925  ioombl1lem4  25528  itg2seq  25709  dvmptdiv  25941  dgrlb  26201  dgrnznn  26212  aaliou2  26306  taylthlem2  26339  cos02pilt1  26490  dvlog2lem  26616  cxple2  26661  mumullem2  27143  chtub  27175  lgsval2lem  27270  lgsdir  27295  lgsne0  27298  lgsqr  27314  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem4  27341  lgsquadlem1  27343  lgsquad2  27349  m1lgs  27351  2sqlem7  27387  2sqblem  27394  nosupbnd1lem1  27672  nosupbnd2  27680  noinfbnd1lem1  27687  noinfbnd2lem1  27694  noinfbnd2  27695  0elold  27902  ltmuls2  28163  pw2cut2  28454  legso  28667  lmiopp  28870  axlowdimlem6  29016  elntg2  29054  1loopgrvd0  29573  1egrvtxdg0  29580  nfrgr2v  30342  nrt2irr  30543  hmdmadj  32011  strlem1  32321  isoun  32775  expgt0b  32890  archirng  33249  rsprprmprmidl  33582  rprmdvdsprod  33594  extdgfialglem1  33836  constrcon  33918  esumrnmpt2  34212  ballotlem4  34643  signswmnd  34701  signslema  34706  bnj1417  35183  satf0n0  35560  fmlaomn0  35572  prv1n  35613  tailfb  36559  weiunfr  36649  unblimceq0  36767  unbdqndv2lem2  36770  qdiff  37641  topdifinffinlem  37663  icorempo  37667  finxpreclem6  37712  lindsadd  37934  mblfinlem4  37981  3dimlem2  39905  3dimlem3a  39906  3dimlem3OLDN  39908  3dim2  39914  3dim3  39915  lplnnle2at  39987  lplnnlelln  39989  llncvrlpln  40004  lvolnle3at  40028  lvolnlelln  40030  lvolnlelpln  40031  4atlem3  40042  lplncvrlvol  40062  dalem30  40148  dalem35  40153  lhp2at0nle  40481  4atexlemswapqr  40509  ltrncnvel  40588  trlnle  40632  cdleme35sn3a  40905  cdleme46frvlpq  40950  cdlemeg46c  40959  cdlemeg46nlpq  40963  cdleme48gfv  40983  cdlemg7fvbwN  41053  cdlemg4d  41059  cdlemg10a  41086  cdlemg12d  41092  cdlemg27b  41142  cdlemg31d  41146  dihmeetlem6  41755  dochshpsat  41900  dochexmidlem1  41906  mapdindp  42117  lspindp5  42216  dvrelog2b  42505  aks4d1p1p7  42513  aks4d1p6  42520  aks6d1c2p2  42558  aks6d1c5lem1  42575  aks6d1c7lem1  42619  aks6d1c7  42623  xppss12  42670  oexpreposd  42754  mulltgt0d  42927  mullt0b2d  42929  sn-mullt0d  42930  dffltz  43067  cmpfiiin  43129  fnwe2lem2  43479  oninfint  43664  dflim5  43757  relexpmulg  44137  relexp01min  44140  relexpxpmin  44144  cvgdvgrat  44740  difmap  45636  gtnelioc  45921  ltnelicc  45927  gtnelicc  45930  lenelioc  45966  xrgtnelicc  45968  limciccioolb  46051  limcrecl  46059  limcicciooub  46065  limclner  46079  reclimc  46081  sinaover2ne0  46296  icccncfext  46315  jumpncnp  46326  itgsincmulx  46402  stoweidlem26  46454  stoweidlem35  46463  stirlinglem5  46506  dirker2re  46520  dirkerdenne0  46521  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncflem1  46531  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem10  46545  fourierdlem24  46559  fourierdlem25  46560  fourierdlem42  46577  fourierdlem44  46579  fourierdlem53  46587  fourierdlem58  46592  fourierdlem62  46596  fourierdlem76  46610  fourierdlem88  46622  fourierdlem104  46638  etransclem41  46703  etransclem44  46706  hoiqssbllem3  47052  smfmbfcex  47188  fsetprcnexALT  47510  difltmodne  47796  minusmodnep2tmod  47807  modm1p1ne  47824  ichnreuop  47932  fmtnoinf  47999  lighneallem3  48070  lighneallem4  48073  bits0eALTV  48156  oddprmALTV  48163  upgrimpths  48385  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg3kgrtriexlem5  48563  gpg5edgnedg  48606  0nodd  48646  2nodd  48648  lindslinindsimp1  48933  line2ylem  49227  line2xlem  49229