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  2858  eqnbrtrd  5165  rnmptn0  6265  nsuceq0  6468  fvun1  6999  tz7.44-2  8445  oeeulem  8637  onomeneqOLD  9263  supgtoreq  9507  inflb  9526  cantnfp1lem2  9716  cantnflem1  9726  rankxpsuc  9919  cardaleph  10126  cfsuc  10294  cflim2  10300  addnidpi  10938  genpnnp  11042  supaddc  12232  supmul1  12234  nnneneg  12298  indstr2  12966  zbtwnre  12985  xrltnsym  13175  xrlttr  13178  xralrple  13243  supicclub2  13540  flltnz  13847  hashelne0d  14403  hashf1lem1  14490  swrdnd  14688  swrd0  14692  sqrtneglem  15301  rlimno1  15686  binomlem  15861  fprodn0f  16023  ruclem12  16273  dvdsle  16343  2tp1odd  16385  smu01lem  16518  rpexp  16755  oddprm  16843  pythagtriplem11  16858  pythagtriplem13  16860  pcpremul  16876  pczndvds2  16900  pc2dvds  16912  pcmpt  16925  smndex1n0mnd  18937  sgrp2nmndlem5  18954  pmtrdifellem4  19511  psgnunilem1  19525  psgnunilem2  19527  efgredlemc  19777  prmcyg  19926  ablfacrplem  20099  ablfac1eulem  20106  ablsimpgfindlem1  20141  fidomndrng  20790  islbs2  21173  frlmssuvc2  21832  1stccnp  23485  fbasfip  23891  metnrmlem1a  24893  xrhmeo  24990  bndth  25003  ioombl1lem4  25609  itg2seq  25791  dvmptdiv  26026  dgrlb  26289  dgrnznn  26300  aaliou2  26396  taylthlem2  26430  taylthlem2OLD  26431  cos02pilt1  26582  dvlog2lem  26708  cxple2  26753  mumullem2  27237  chtub  27270  lgsval2lem  27365  lgsdir  27390  lgsne0  27393  lgsqr  27409  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem4  27436  lgsquadlem1  27438  lgsquad2  27444  m1lgs  27446  2sqlem7  27482  2sqblem  27489  nosupbnd1lem1  27767  nosupbnd2  27775  noinfbnd1lem1  27782  noinfbnd2lem1  27789  noinfbnd2  27790  0elold  27961  sltmul2  28211  legso  28621  lmiopp  28824  axlowdimlem6  28976  elntg2  29014  1loopgrvd0  29536  1egrvtxdg0  29543  nfrgr2v  30300  nrt2irr  30501  hmdmadj  31968  strlem1  32278  isoun  32716  expgt0b  32822  archirng  33177  rsprprmprmidl  33529  rprmdvdsprod  33541  esumrnmpt2  34048  ballotlem4  34479  signswmnd  34550  signslema  34555  bnj1417  35033  satf0n0  35362  fmlaomn0  35374  prv1n  35415  tailfb  36359  weiunfr  36449  unblimceq0  36489  unbdqndv2lem2  36492  topdifinffinlem  37329  icorempo  37333  finxpreclem6  37378  lindsadd  37599  mblfinlem4  37646  3dimlem2  39441  3dimlem3a  39442  3dimlem3OLDN  39444  3dim2  39450  3dim3  39451  lplnnle2at  39523  lplnnlelln  39525  llncvrlpln  39540  lvolnle3at  39564  lvolnlelln  39566  lvolnlelpln  39567  4atlem3  39578  lplncvrlvol  39598  dalem30  39684  dalem35  39689  lhp2at0nle  40017  4atexlemswapqr  40045  ltrncnvel  40124  trlnle  40168  cdleme35sn3a  40441  cdleme46frvlpq  40486  cdlemeg46c  40495  cdlemeg46nlpq  40499  cdleme48gfv  40519  cdlemg7fvbwN  40589  cdlemg4d  40595  cdlemg10a  40622  cdlemg12d  40628  cdlemg27b  40678  cdlemg31d  40682  dihmeetlem6  41291  dochshpsat  41436  dochexmidlem1  41442  mapdindp  41653  lspindp5  41752  dvrelog2b  42047  aks4d1p1p7  42055  aks4d1p6  42062  aks6d1c2p2  42100  aks6d1c5lem1  42117  aks6d1c7lem1  42161  aks6d1c7  42165  metakunt30  42215  xppss12  42246  oexpreposd  42335  dffltz  42620  cmpfiiin  42684  fnwe2lem2  43039  oninfint  43224  dflim5  43318  relexpmulg  43699  relexp01min  43702  relexpxpmin  43706  cvgdvgrat  44308  nelrnmpt  45023  difmap  45149  gtnelioc  45443  ltnelicc  45449  gtnelicc  45452  lenelioc  45488  xrgtnelicc  45490  limciccioolb  45576  limcrecl  45584  limcicciooub  45592  limclner  45606  reclimc  45608  sinaover2ne0  45823  icccncfext  45842  jumpncnp  45853  itgsincmulx  45929  stoweidlem26  45981  stoweidlem35  45990  stirlinglem5  46033  dirker2re  46047  dirkerdenne0  46048  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncflem1  46058  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem10  46072  fourierdlem24  46086  fourierdlem25  46087  fourierdlem42  46104  fourierdlem44  46106  fourierdlem53  46114  fourierdlem58  46119  fourierdlem62  46123  fourierdlem76  46137  fourierdlem88  46149  fourierdlem104  46165  etransclem41  46230  etransclem44  46233  hoiqssbllem3  46579  smfmbfcex  46715  fsetprcnexALT  47011  difltmodne  47281  minusmodnep2tmod  47292  ichnreuop  47396  fmtnoinf  47460  lighneallem3  47531  lighneallem4  47534  bits0eALTV  47604  oddprmALTV  47611  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  0nodd  48013  2nodd  48015  lindslinindsimp1  48302  line2ylem  48600  line2xlem  48602