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  2848  eqnbrtrd  5113  rnmptn0  6197  nsuceq0  6396  fvun1  6918  tz7.44-2  8336  oeeulem  8526  supgtoreq  9380  inflb  9399  cantnfp1lem2  9594  cantnflem1  9604  rankxpsuc  9797  cardaleph  10002  cfsuc  10170  cflim2  10176  addnidpi  10814  genpnnp  10918  supaddc  12110  supmul1  12112  nnneneg  12181  indstr2  12846  zbtwnre  12865  xrltnsym  13057  xrlttr  13060  xralrple  13125  supicclub2  13425  flltnz  13733  hashelne0d  14293  hashf1lem1  14380  swrdnd  14579  swrd0  14583  sqrtneglem  15191  rlimno1  15579  binomlem  15754  fprodn0f  15916  ruclem12  16168  dvdsle  16239  2tp1odd  16281  smu01lem  16414  rpexp  16651  oddprm  16740  pythagtriplem11  16755  pythagtriplem13  16757  pcpremul  16773  pczndvds2  16797  pc2dvds  16809  pcmpt  16822  smndex1n0mnd  18804  sgrp2nmndlem5  18821  pmtrdifellem4  19376  psgnunilem1  19390  psgnunilem2  19392  efgredlemc  19642  prmcyg  19791  ablfacrplem  19964  ablfac1eulem  19971  ablsimpgfindlem1  20006  fidomndrng  20676  islbs2  21079  frlmssuvc2  21720  1stccnp  23365  fbasfip  23771  metnrmlem1a  24763  xrhmeo  24860  bndth  24873  ioombl1lem4  25478  itg2seq  25659  dvmptdiv  25894  dgrlb  26157  dgrnznn  26168  aaliou2  26264  taylthlem2  26298  taylthlem2OLD  26299  cos02pilt1  26451  dvlog2lem  26577  cxple2  26622  mumullem2  27106  chtub  27139  lgsval2lem  27234  lgsdir  27259  lgsne0  27262  lgsqr  27278  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem4  27305  lgsquadlem1  27307  lgsquad2  27313  m1lgs  27315  2sqlem7  27351  2sqblem  27358  nosupbnd1lem1  27636  nosupbnd2  27644  noinfbnd1lem1  27651  noinfbnd2lem1  27658  noinfbnd2  27659  0elold  27842  sltmul2  28097  legso  28562  lmiopp  28765  axlowdimlem6  28910  elntg2  28948  1loopgrvd0  29468  1egrvtxdg0  29475  nfrgr2v  30234  nrt2irr  30435  hmdmadj  31902  strlem1  32212  isoun  32658  expgt0b  32774  archirng  33140  rsprprmprmidl  33469  rprmdvdsprod  33481  constrcon  33740  esumrnmpt2  34034  ballotlem4  34466  signswmnd  34524  signslema  34529  bnj1417  35007  satf0n0  35350  fmlaomn0  35362  prv1n  35403  tailfb  36350  weiunfr  36440  unblimceq0  36480  unbdqndv2lem2  36483  topdifinffinlem  37320  icorempo  37324  finxpreclem6  37369  lindsadd  37592  mblfinlem4  37639  3dimlem2  39438  3dimlem3a  39439  3dimlem3OLDN  39441  3dim2  39447  3dim3  39448  lplnnle2at  39520  lplnnlelln  39522  llncvrlpln  39537  lvolnle3at  39561  lvolnlelln  39563  lvolnlelpln  39564  4atlem3  39575  lplncvrlvol  39595  dalem30  39681  dalem35  39686  lhp2at0nle  40014  4atexlemswapqr  40042  ltrncnvel  40121  trlnle  40165  cdleme35sn3a  40438  cdleme46frvlpq  40483  cdlemeg46c  40492  cdlemeg46nlpq  40496  cdleme48gfv  40516  cdlemg7fvbwN  40586  cdlemg4d  40592  cdlemg10a  40619  cdlemg12d  40625  cdlemg27b  40675  cdlemg31d  40679  dihmeetlem6  41288  dochshpsat  41433  dochexmidlem1  41439  mapdindp  41650  lspindp5  41749  dvrelog2b  42039  aks4d1p1p7  42047  aks4d1p6  42054  aks6d1c2p2  42092  aks6d1c5lem1  42109  aks6d1c7lem1  42153  aks6d1c7  42157  xppss12  42202  oexpreposd  42295  mulltgt0d  42455  mullt0b2d  42457  sn-mullt0d  42458  dffltz  42607  cmpfiiin  42670  fnwe2lem2  43024  oninfint  43209  dflim5  43302  relexpmulg  43683  relexp01min  43686  relexpxpmin  43690  cvgdvgrat  44286  nelrnmpt  45062  difmap  45185  gtnelioc  45473  ltnelicc  45479  gtnelicc  45482  lenelioc  45518  xrgtnelicc  45520  limciccioolb  45603  limcrecl  45611  limcicciooub  45619  limclner  45633  reclimc  45635  sinaover2ne0  45850  icccncfext  45869  jumpncnp  45880  itgsincmulx  45956  stoweidlem26  46008  stoweidlem35  46017  stirlinglem5  46060  dirker2re  46074  dirkerdenne0  46075  dirkertrigeqlem3  46082  dirkertrigeq  46083  dirkercncflem1  46085  dirkercncflem2  46086  dirkercncflem4  46088  fourierdlem10  46099  fourierdlem24  46113  fourierdlem25  46114  fourierdlem42  46131  fourierdlem44  46133  fourierdlem53  46141  fourierdlem58  46146  fourierdlem62  46150  fourierdlem76  46164  fourierdlem88  46176  fourierdlem104  46192  etransclem41  46257  etransclem44  46260  hoiqssbllem3  46606  smfmbfcex  46742  fsetprcnexALT  47047  difltmodne  47327  minusmodnep2tmod  47338  modm1p1ne  47355  ichnreuop  47457  fmtnoinf  47521  lighneallem3  47592  lighneallem4  47595  bits0eALTV  47665  oddprmALTV  47672  upgrimpths  47894  gpg5nbgrvtx03starlem1  48053  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx03starlem3  48055  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem2  48057  gpg5nbgrvtx13starlem3  48058  gpg3kgrtriexlem5  48072  gpg5edgnedg  48115  0nodd  48155  2nodd  48157  lindslinindsimp1  48443  line2ylem  48737  line2xlem  48739