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  2857  eqnbrtrd  5118  nelrnmpt  5924  rnmptn0  6210  nsuceq0  6410  fvun1  6933  tz7.44-2  8348  oeeulem  8539  supgtoreq  9386  inflb  9405  cantnfp1lem2  9600  cantnflem1  9610  rankxpsuc  9806  cardaleph  10011  cfsuc  10179  cflim2  10185  addnidpi  10824  genpnnp  10928  supaddc  12121  supmul1  12123  nnneneg  12192  indstr2  12852  zbtwnre  12871  xrltnsym  13063  xrlttr  13066  xralrple  13132  supicclub2  13432  flltnz  13743  hashelne0d  14303  hashf1lem1  14390  swrdnd  14590  swrd0  14594  sqrtneglem  15201  rlimno1  15589  binomlem  15764  fprodn0f  15926  ruclem12  16178  dvdsle  16249  2tp1odd  16291  smu01lem  16424  rpexp  16661  oddprm  16750  pythagtriplem11  16765  pythagtriplem13  16767  pcpremul  16783  pczndvds2  16807  pc2dvds  16819  pcmpt  16832  smndex1n0mnd  18849  sgrp2nmndlem5  18866  pmtrdifellem4  19420  psgnunilem1  19434  psgnunilem2  19436  efgredlemc  19686  prmcyg  19835  ablfacrplem  20008  ablfac1eulem  20015  ablsimpgfindlem1  20050  fidomndrng  20718  islbs2  21121  frlmssuvc2  21762  1stccnp  23418  fbasfip  23824  metnrmlem1a  24815  xrhmeo  24912  bndth  24925  ioombl1lem4  25530  itg2seq  25711  dvmptdiv  25946  dgrlb  26209  dgrnznn  26220  aaliou2  26316  taylthlem2  26350  taylthlem2OLD  26351  cos02pilt1  26503  dvlog2lem  26629  cxple2  26674  mumullem2  27158  chtub  27191  lgsval2lem  27286  lgsdir  27311  lgsne0  27314  lgsqr  27330  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem4  27357  lgsquadlem1  27359  lgsquad2  27365  m1lgs  27367  2sqlem7  27403  2sqblem  27410  nosupbnd1lem1  27688  nosupbnd2  27696  noinfbnd1lem1  27703  noinfbnd2lem1  27710  noinfbnd2  27711  0elold  27918  ltmuls2  28179  pw2cut2  28470  legso  28683  lmiopp  28886  axlowdimlem6  29032  elntg2  29070  1loopgrvd0  29590  1egrvtxdg0  29597  nfrgr2v  30359  nrt2irr  30560  hmdmadj  32027  strlem1  32337  isoun  32791  expgt0b  32907  archirng  33281  rsprprmprmidl  33614  rprmdvdsprod  33626  extdgfialglem1  33869  constrcon  33951  esumrnmpt2  34245  ballotlem4  34676  signswmnd  34734  signslema  34739  bnj1417  35216  satf0n0  35591  fmlaomn0  35603  prv1n  35644  tailfb  36590  weiunfr  36680  unblimceq0  36726  unbdqndv2lem2  36729  topdifinffinlem  37596  icorempo  37600  finxpreclem6  37645  lindsadd  37858  mblfinlem4  37905  3dimlem2  39829  3dimlem3a  39830  3dimlem3OLDN  39832  3dim2  39838  3dim3  39839  lplnnle2at  39911  lplnnlelln  39913  llncvrlpln  39928  lvolnle3at  39952  lvolnlelln  39954  lvolnlelpln  39955  4atlem3  39966  lplncvrlvol  39986  dalem30  40072  dalem35  40077  lhp2at0nle  40405  4atexlemswapqr  40433  ltrncnvel  40512  trlnle  40556  cdleme35sn3a  40829  cdleme46frvlpq  40874  cdlemeg46c  40883  cdlemeg46nlpq  40887  cdleme48gfv  40907  cdlemg7fvbwN  40977  cdlemg4d  40983  cdlemg10a  41010  cdlemg12d  41016  cdlemg27b  41066  cdlemg31d  41070  dihmeetlem6  41679  dochshpsat  41824  dochexmidlem1  41830  mapdindp  42041  lspindp5  42140  dvrelog2b  42430  aks4d1p1p7  42438  aks4d1p6  42445  aks6d1c2p2  42483  aks6d1c5lem1  42500  aks6d1c7lem1  42544  aks6d1c7  42548  xppss12  42595  oexpreposd  42686  mulltgt0d  42846  mullt0b2d  42848  sn-mullt0d  42849  dffltz  42986  cmpfiiin  43048  fnwe2lem2  43402  oninfint  43587  dflim5  43680  relexpmulg  44060  relexp01min  44063  relexpxpmin  44067  cvgdvgrat  44663  difmap  45559  gtnelioc  45845  ltnelicc  45851  gtnelicc  45854  lenelioc  45890  xrgtnelicc  45892  limciccioolb  45975  limcrecl  45983  limcicciooub  45989  limclner  46003  reclimc  46005  sinaover2ne0  46220  icccncfext  46239  jumpncnp  46250  itgsincmulx  46326  stoweidlem26  46378  stoweidlem35  46387  stirlinglem5  46430  dirker2re  46444  dirkerdenne0  46445  dirkertrigeqlem3  46452  dirkertrigeq  46453  dirkercncflem1  46455  dirkercncflem2  46456  dirkercncflem4  46458  fourierdlem10  46469  fourierdlem24  46483  fourierdlem25  46484  fourierdlem42  46501  fourierdlem44  46503  fourierdlem53  46511  fourierdlem58  46516  fourierdlem62  46520  fourierdlem76  46534  fourierdlem88  46546  fourierdlem104  46562  etransclem41  46627  etransclem44  46630  hoiqssbllem3  46976  smfmbfcex  47112  fsetprcnexALT  47416  difltmodne  47696  minusmodnep2tmod  47707  modm1p1ne  47724  ichnreuop  47826  fmtnoinf  47890  lighneallem3  47961  lighneallem4  47964  bits0eALTV  48034  oddprmALTV  48041  upgrimpths  48263  gpg5nbgrvtx03starlem1  48422  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx03starlem3  48424  gpg5nbgrvtx13starlem1  48425  gpg5nbgrvtx13starlem2  48426  gpg5nbgrvtx13starlem3  48427  gpg3kgrtriexlem5  48441  gpg5edgnedg  48484  0nodd  48524  2nodd  48526  lindslinindsimp1  48811  line2ylem  49105  line2xlem  49107