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  2861  eqnbrtrd  5161  rnmptn0  6264  nsuceq0  6467  fvun1  7000  tz7.44-2  8447  oeeulem  8639  onomeneqOLD  9266  supgtoreq  9510  inflb  9529  cantnfp1lem2  9719  cantnflem1  9729  rankxpsuc  9922  cardaleph  10129  cfsuc  10297  cflim2  10303  addnidpi  10941  genpnnp  11045  supaddc  12235  supmul1  12237  nnneneg  12301  indstr2  12969  zbtwnre  12988  xrltnsym  13179  xrlttr  13182  xralrple  13247  supicclub2  13544  flltnz  13851  hashelne0d  14407  hashf1lem1  14494  swrdnd  14692  swrd0  14696  sqrtneglem  15305  rlimno1  15690  binomlem  15865  fprodn0f  16027  ruclem12  16277  dvdsle  16347  2tp1odd  16389  smu01lem  16522  rpexp  16759  oddprm  16848  pythagtriplem11  16863  pythagtriplem13  16865  pcpremul  16881  pczndvds2  16905  pc2dvds  16917  pcmpt  16930  smndex1n0mnd  18925  sgrp2nmndlem5  18942  pmtrdifellem4  19497  psgnunilem1  19511  psgnunilem2  19513  efgredlemc  19763  prmcyg  19912  ablfacrplem  20085  ablfac1eulem  20092  ablsimpgfindlem1  20127  fidomndrng  20774  islbs2  21156  frlmssuvc2  21815  1stccnp  23470  fbasfip  23876  metnrmlem1a  24880  xrhmeo  24977  bndth  24990  ioombl1lem4  25596  itg2seq  25777  dvmptdiv  26012  dgrlb  26275  dgrnznn  26286  aaliou2  26382  taylthlem2  26416  taylthlem2OLD  26417  cos02pilt1  26568  dvlog2lem  26694  cxple2  26739  mumullem2  27223  chtub  27256  lgsval2lem  27351  lgsdir  27376  lgsne0  27379  lgsqr  27395  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem4  27422  lgsquadlem1  27424  lgsquad2  27430  m1lgs  27432  2sqlem7  27468  2sqblem  27475  nosupbnd1lem1  27753  nosupbnd2  27761  noinfbnd1lem1  27768  noinfbnd2lem1  27775  noinfbnd2  27776  0elold  27947  sltmul2  28197  legso  28607  lmiopp  28810  axlowdimlem6  28962  elntg2  29000  1loopgrvd0  29522  1egrvtxdg0  29529  nfrgr2v  30291  nrt2irr  30492  hmdmadj  31959  strlem1  32269  isoun  32711  expgt0b  32818  archirng  33195  rsprprmprmidl  33550  rprmdvdsprod  33562  esumrnmpt2  34069  ballotlem4  34501  signswmnd  34572  signslema  34577  bnj1417  35055  satf0n0  35383  fmlaomn0  35395  prv1n  35436  tailfb  36378  weiunfr  36468  unblimceq0  36508  unbdqndv2lem2  36511  topdifinffinlem  37348  icorempo  37352  finxpreclem6  37397  lindsadd  37620  mblfinlem4  37667  3dimlem2  39461  3dimlem3a  39462  3dimlem3OLDN  39464  3dim2  39470  3dim3  39471  lplnnle2at  39543  lplnnlelln  39545  llncvrlpln  39560  lvolnle3at  39584  lvolnlelln  39586  lvolnlelpln  39587  4atlem3  39598  lplncvrlvol  39618  dalem30  39704  dalem35  39709  lhp2at0nle  40037  4atexlemswapqr  40065  ltrncnvel  40144  trlnle  40188  cdleme35sn3a  40461  cdleme46frvlpq  40506  cdlemeg46c  40515  cdlemeg46nlpq  40519  cdleme48gfv  40539  cdlemg7fvbwN  40609  cdlemg4d  40615  cdlemg10a  40642  cdlemg12d  40648  cdlemg27b  40698  cdlemg31d  40702  dihmeetlem6  41311  dochshpsat  41456  dochexmidlem1  41462  mapdindp  41673  lspindp5  41772  dvrelog2b  42067  aks4d1p1p7  42075  aks4d1p6  42082  aks6d1c2p2  42120  aks6d1c5lem1  42137  aks6d1c7lem1  42181  aks6d1c7  42185  metakunt30  42235  xppss12  42268  oexpreposd  42357  dffltz  42644  cmpfiiin  42708  fnwe2lem2  43063  oninfint  43248  dflim5  43342  relexpmulg  43723  relexp01min  43726  relexpxpmin  43730  cvgdvgrat  44332  nelrnmpt  45089  difmap  45212  gtnelioc  45504  ltnelicc  45510  gtnelicc  45513  lenelioc  45549  xrgtnelicc  45551  limciccioolb  45636  limcrecl  45644  limcicciooub  45652  limclner  45666  reclimc  45668  sinaover2ne0  45883  icccncfext  45902  jumpncnp  45913  itgsincmulx  45989  stoweidlem26  46041  stoweidlem35  46050  stirlinglem5  46093  dirker2re  46107  dirkerdenne0  46108  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem1  46118  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem10  46132  fourierdlem24  46146  fourierdlem25  46147  fourierdlem42  46164  fourierdlem44  46166  fourierdlem53  46174  fourierdlem58  46179  fourierdlem62  46183  fourierdlem76  46197  fourierdlem88  46209  fourierdlem104  46225  etransclem41  46290  etransclem44  46293  hoiqssbllem3  46639  smfmbfcex  46775  fsetprcnexALT  47074  difltmodne  47344  minusmodnep2tmod  47355  ichnreuop  47459  fmtnoinf  47523  lighneallem3  47594  lighneallem4  47597  bits0eALTV  47667  oddprmALTV  47674  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  gpg3kgrtriexlem5  48043  0nodd  48086  2nodd  48088  lindslinindsimp1  48374  line2ylem  48672  line2xlem  48674