Theorem mtbird 327

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  eqneltrd  2881  eqnbrtrd  5117  nelrnmpt  5941  rnmptn0  6227  nsuceq0  6427  fvun1  6954  tz7.44-2  8373  oeeulem  8566  supgtoreq  9414  inflb  9433  cantnfp1lem2  9631  cantnflem1  9641  rankxpsuc  9837  cardaleph  10042  cfsuc  10211  cflim2  10217  addnidpi  10856  genpnnp  10960  supaddc  12156  supmul1  12158  nnneneg  12245  indstr2  12925  zbtwnre  12944  xrltnsym  13136  xrlttr  13139  xralrple  13205  supicclub2  13505  flltnz  13818  hashelne0d  14378  hashf1lem1  14465  swrdnd  14665  swrd0  14669  sqrtneglem  15276  rlimno1  15664  binomlem  15842  fprodn0f  16004  ruclem12  16256  dvdsle  16327  2tp1odd  16369  smu01lem  16502  rpexp  16740  oddprm  16829  pythagtriplem11  16844  pythagtriplem13  16846  pcpremul  16862  pczndvds2  16886  pc2dvds  16898  pcmpt  16911  smndex1n0mnd  18932  sgrp2nmndlem5  18949  pmtrdifellem4  19502  psgnunilem1  19516  psgnunilem2  19518  efgredlemc  19768  prmcyg  19917  ablfacrplem  20090  ablfac1eulem  20097  ablsimpgfindlem1  20132  fidomndrng  20802  islbs2  21204  frlmssuvc2  21827  1stccnp  23502  fbasfip  23908  metnrmlem1a  24899  xrhmeo  24988  bndth  25000  ioombl1lem4  25603  itg2seq  25784  dvmptdiv  26016  dgrlb  26276  dgrnznn  26287  aaliou2  26381  taylthlem2  26414  cos02pilt1  26568  dvlog2lem  26694  cxple2  26739  mumullem2  27221  chtub  27253  lgsval2lem  27348  lgsdir  27373  lgsne0  27376  lgsqr  27392  lgseisenlem1  27416  lgseisenlem2  27417  lgseisenlem4  27419  lgsquadlem1  27421  lgsquad2  27427  m1lgs  27429  2sqlem7  27465  2sqblem  27472  nosupbnd1lem1  27749  nosupbnd2  27757  noinfbnd1lem1  27764  noinfbnd2lem1  27771  noinfbnd2  27772  0elold  27980  ltmuls2  28241  pw2cut2  28532  legso  28745  lmiopp  28948  axlowdimlem6  29094  elntg2  29132  1loopgrvd0  29651  1egrvtxdg0  29658  nfrgr2v  30420  nrt2irr  30621  hmdmadj  32089  strlem1  32399  isoun  32854  expgt0b  32969  archirng  33329  rsprprmprmidl  33679  rprmdvdsprod  33691  extdgfialglem1  33950  constrcon  34032  esumrnmpt2  34326  ballotlem4  34757  signswmnd  34815  signslema  34820  bnj1417  35300  satf0n0  35692  fmlaomn0  35704  prv1n  35745  tailfb  36701  weiunfr  36791  unblimceq0  36909  unbdqndv2lem2  36912  qdiff  37783  topdifinffinlem  37805  icorempo  37809  finxpreclem6  37854  lindsadd  38076  mblfinlem4  38123  3dimlem2  40047  3dimlem3a  40048  3dimlem3OLDN  40050  3dim2  40056  3dim3  40057  lplnnle2at  40129  lplnnlelln  40131  llncvrlpln  40146  lvolnle3at  40170  lvolnlelln  40172  lvolnlelpln  40173  4atlem3  40184  lplncvrlvol  40204  dalem30  40290  dalem35  40295  lhp2at0nle  40623  4atexlemswapqr  40651  ltrncnvel  40730  trlnle  40774  cdleme35sn3a  41047  cdleme46frvlpq  41092  cdlemeg46c  41101  cdlemeg46nlpq  41105  cdleme48gfv  41125  cdlemg7fvbwN  41195  cdlemg4d  41201  cdlemg10a  41228  cdlemg12d  41234  cdlemg27b  41284  cdlemg31d  41288  dihmeetlem6  41897  dochshpsat  42042  dochexmidlem1  42048  mapdindp  42259  lspindp5  42358  dvrelog2b  42647  aks4d1p1p7  42655  aks4d1p6  42662  aks6d1c2p2  42700  aks6d1c5lem1  42717  aks6d1c7lem1  42761  aks6d1c7  42765  xppss12  42812  oexpreposd  42895  mulltgt0d  43068  mullt0b2d  43070  sn-mullt0d  43071  dffltz  43180  cmpfiiin  43242  fnwe2lem2  43592  oninfint  43777  dflim5  43870  relexpmulg  44250  relexp01min  44253  relexpxpmin  44257  cvgdvgrat  44853  difmap  45747  gtnelioc  46031  ltnelicc  46037  gtnelicc  46040  lenelioc  46076  xrgtnelicc  46078  limciccioolb  46161  limcrecl  46169  limcicciooub  46175  limclner  46189  reclimc  46191  sinaover2ne0  46406  icccncfext  46425  jumpncnp  46436  itgsincmulx  46512  stoweidlem26  46564  stoweidlem35  46573  stirlinglem5  46616  dirker2re  46630  dirkerdenne0  46631  dirkertrigeqlem3  46638  dirkertrigeq  46639  dirkercncflem1  46641  dirkercncflem2  46642  dirkercncflem4  46644  fourierdlem10  46655  fourierdlem24  46669  fourierdlem25  46670  fourierdlem42  46687  fourierdlem44  46689  fourierdlem53  46697  fourierdlem58  46702  fourierdlem62  46706  fourierdlem76  46720  fourierdlem88  46732  fourierdlem104  46748  etransclem41  46813  etransclem44  46816  hoiqssbllem3  47162  smfmbfcex  47298  fsetprcnexALT  47620  difltmodne  47906  minusmodnep2tmod  47917  modm1p1ne  47934  ichnreuop  48042  fmtnoinf  48109  lighneallem3  48180  lighneallem4  48183  bits0eALTV  48266  oddprmALTV  48273  upgrimpths  48495  gpg5nbgrvtx03starlem1  48654  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx03starlem3  48656  gpg5nbgrvtx13starlem1  48657  gpg5nbgrvtx13starlem2  48658  gpg5nbgrvtx13starlem3  48659  gpg3kgrtriexlem5  48673  gpg5edgnedg  48716  0nodd  48756  2nodd  48758  lindslinindsimp1  49043  line2ylem  49337  line2xlem  49339