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

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

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 206

This theorem is referenced by:  eqneltrd  2859  eqnbrtrd  5093  rnmptn0  6152  nsuceq0  6350  fvun1  6868  tz7.44-2  8247  oeeulem  8441  onomeneqOLD  9021  supgtoreq  9238  inflb  9257  cantnfp1lem2  9446  cantnflem1  9456  rankxpsuc  9649  cardaleph  9854  cfsuc  10022  cflim2  10028  addnidpi  10666  genpnnp  10770  supaddc  11951  supmul1  11953  nnneneg  12017  indstr2  12676  zbtwnre  12695  xrltnsym  12880  xrlttr  12883  xralrple  12948  supicclub2  13245  flltnz  13540  hashelne0d  14092  hashf1lem1  14177  hashf1lem1OLD  14178  swrdnd  14376  swrd0  14380  sqrtneglem  14987  rlimno1  15374  binomlem  15550  fprodn0f  15710  ruclem12  15959  dvdsle  16028  2tp1odd  16070  smu01lem  16201  rpexp  16436  oddprm  16520  pythagtriplem11  16535  pythagtriplem13  16537  pcpremul  16553  pczndvds2  16577  pc2dvds  16589  pcmpt  16602  smndex1n0mnd  18560  sgrp2nmndlem5  18577  pmtrdifellem4  19096  psgnunilem1  19110  psgnunilem2  19112  efgredlemc  19360  prmcyg  19504  ablfacrplem  19677  ablfac1eulem  19684  ablsimpgfindlem1  19719  islbs2  20425  fidomndrng  20588  frlmssuvc2  21011  1stccnp  22622  fbasfip  23028  metnrmlem1a  24030  xrhmeo  24118  bndth  24130  ioombl1lem4  24734  itg2seq  24916  dvmptdiv  25147  dgrlb  25406  dgrnznn  25417  aaliou2  25509  taylthlem2  25542  cos02pilt1  25691  dvlog2lem  25816  cxple2  25861  mumullem2  26338  chtub  26369  lgsval2lem  26464  lgsdir  26489  lgsne0  26492  lgsqr  26508  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem4  26535  lgsquadlem1  26537  lgsquad2  26543  m1lgs  26545  2sqlem7  26581  2sqblem  26588  legso  26969  lmiopp  27172  axlowdimlem6  27324  elntg2  27362  1loopgrvd0  27880  1egrvtxdg0  27887  nfrgr2v  28645  hmdmadj  30311  strlem1  30621  isoun  31043  archirng  31451  esumrnmpt2  32045  ballotlem4  32474  signswmnd  32545  signslema  32550  bnj1417  33030  satf0n0  33349  fmlaomn0  33361  prv1n  33402  nosupbnd1lem1  33920  nosupbnd2  33928  noinfbnd1lem1  33935  noinfbnd2lem1  33942  noinfbnd2  33943  tailfb  34575  unblimceq0  34696  unbdqndv2lem2  34699  topdifinffinlem  35527  icorempo  35531  finxpreclem6  35576  lindsadd  35779  mblfinlem4  35826  3dimlem2  37480  3dimlem3a  37481  3dimlem3OLDN  37483  3dim2  37489  3dim3  37490  lplnnle2at  37562  lplnnlelln  37564  llncvrlpln  37579  lvolnle3at  37603  lvolnlelln  37605  lvolnlelpln  37606  4atlem3  37617  lplncvrlvol  37637  dalem30  37723  dalem35  37728  lhp2at0nle  38056  4atexlemswapqr  38084  ltrncnvel  38163  trlnle  38207  cdleme35sn3a  38480  cdleme46frvlpq  38525  cdlemeg46c  38534  cdlemeg46nlpq  38538  cdleme48gfv  38558  cdlemg7fvbwN  38628  cdlemg4d  38634  cdlemg10a  38661  cdlemg12d  38667  cdlemg27b  38717  cdlemg31d  38721  dihmeetlem6  39330  dochshpsat  39475  dochexmidlem1  39481  mapdindp  39692  lspindp5  39791  dvrelog2b  40081  aks4d1p1p7  40089  aks4d1p6  40096  metakunt30  40161  xppss12  40211  oexpreposd  40328  dffltz  40478  cmpfiiin  40526  fnwe2lem2  40883  relexpmulg  41325  relexp01min  41328  relexpxpmin  41332  cvgdvgrat  41938  nelrnmpt  42641  difmap  42754  gtnelioc  43036  ltnelicc  43042  gtnelicc  43045  lenelioc  43081  xrgtnelicc  43083  limciccioolb  43169  limcrecl  43177  limcicciooub  43185  limclner  43199  reclimc  43201  sinaover2ne0  43416  icccncfext  43435  jumpncnp  43446  itgsincmulx  43522  stoweidlem26  43574  stoweidlem35  43583  stirlinglem5  43626  dirker2re  43640  dirkerdenne0  43641  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkercncflem1  43651  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem10  43665  fourierdlem24  43679  fourierdlem25  43680  fourierdlem42  43697  fourierdlem44  43699  fourierdlem53  43707  fourierdlem58  43712  fourierdlem62  43716  fourierdlem76  43730  fourierdlem88  43742  fourierdlem104  43758  etransclem41  43823  etransclem44  43826  hoiqssbllem3  44169  smfmbfcex  44305  fsetprcnexALT  44567  ichnreuop  44935  fmtnoinf  44999  lighneallem3  45070  lighneallem4  45073  bits0eALTV  45143  oddprmALTV  45150  0nodd  45375  2nodd  45377  lindslinindsimp1  45809  line2ylem  46108  line2xlem  46110