Theorem mtbird 315

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

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

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 197

This theorem is referenced by:  eqneltrd  2720  nelsnOLD  4213  eqnbrtrd  4671  nsuceq0  5805  fvun1  6269  tz7.44-2  7503  oeeulem  7681  onomeneq  8150  supgtoreq  8376  inflb  8395  cantnfp1lem2  8576  cantnflem1  8586  rankxpsuc  8745  cardaleph  8912  cfsuc  9079  cflim2  9085  addnidpi  9723  genpnnp  9827  supaddc  10990  supmul1  10992  indstr2  11767  zbtwnre  11786  xrltnsym  11970  xrlttr  11973  xralrple  12036  supicclub2  12323  flltnz  12612  hashf1lem1  13239  swrdnd  13432  swrd0  13434  sqrtneglem  14007  rlimno1  14384  binomlem  14561  fprodn0f  14722  ruclem12  14970  dvdsle  15032  2tp1odd  15076  smu01lem  15207  rpexp  15432  oddprm  15515  pythagtriplem11  15530  pythagtriplem13  15532  pcpremul  15548  pczndvds  15569  pczndvds2  15571  pc2dvds  15583  pcadd  15593  pcmpt  15596  sgrp2nmndlem5  17416  pmtrdifellem4  17899  psgnunilem1  17913  psgnunilem2  17915  efgredlemc  18158  prmcyg  18295  ablfacrplem  18464  ablfac1eulem  18471  islbs2  19154  fidomndrng  19307  frlmssuvc2  20134  1stccnp  21265  fbasfip  21672  recld2  22617  metnrmlem1a  22661  xrhmeo  22745  bndth  22757  ioombl1lem4  23329  itg2seq  23509  itg2cnlem2  23529  dvmptdiv  23737  dgrub  23990  dgrlb  23992  dgrnznn  24003  aaliou2  24095  taylthlem2  24128  dvlog2lem  24398  cxple2  24443  mumullem2  24906  chtub  24937  lgsval2lem  25032  lgsdir  25057  lgsne0  25060  lgsqr  25076  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem4  25103  lgsquadlem1  25105  lgsquad2  25111  m1lgs  25113  2sqlem7  25149  2sqblem  25156  legso  25494  mirbtwnhl  25575  lmiopp  25694  axlowdimlem6  25827  1loopgrvd0  26400  1egrvtxdg0  26407  nfrgr2v  27136  frgrncvvdeqlem1  27163  hmdmadj  28799  strlem1  29109  isoun  29479  archirng  29742  esumrnmpt2  30130  ballotlem4  30560  signswmnd  30634  signslema  30639  bnj1417  31109  nosupbnd1lem1  31854  nosupbnd2  31862  tailfb  32372  unblimceq0  32498  unbdqndv2lem2  32501  topdifinffinlem  33195  icorempt2  33199  finxpreclem6  33233  mblfinlem4  33449  3dimlem2  34745  3dimlem3a  34746  3dimlem3OLDN  34748  3dim2  34754  3dim3  34755  lplnnle2at  34827  lplnnlelln  34829  llncvrlpln  34844  lvolnle3at  34868  lvolnlelln  34870  lvolnlelpln  34871  4atlem3  34882  lplncvrlvol  34902  dalem30  34988  dalem35  34993  lhp2at0nle  35321  4atexlemswapqr  35349  ltrncnvel  35428  trlnle  35473  cdleme35sn3a  35747  cdleme46frvlpq  35792  cdlemeg46c  35801  cdlemeg46nlpq  35805  cdleme48gfv  35825  cdlemg7fvbwN  35895  cdlemg4d  35901  cdlemg10a  35928  cdlemg12d  35934  cdlemg27b  35984  cdlemg31d  35988  dihmeetlem6  36598  dochshpsat  36743  dochexmidlem1  36749  mapdindp  36960  lspindp5  37059  cmpfiiin  37260  fnwe2lem2  37621  relexpmulg  38002  relexp01min  38005  relexpxpmin  38009  cvgdvgrat  38512  nelrnmpt  39257  difmap  39399  rnmptn0  39413  gtnelioc  39712  ltnelicc  39719  gtnelicc  39722  lenelioc  39763  xrgtnelicc  39765  limciccioolb  39853  limcrecl  39861  limcicciooub  39869  limclner  39883  reclimc  39885  sinaover2ne0  40079  icccncfext  40100  jumpncnp  40111  itgsincmulx  40190  stoweidlem26  40243  stoweidlem35  40252  stirlinglem5  40295  dirker2re  40309  dirkerdenne0  40310  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem10  40334  fourierdlem24  40348  fourierdlem25  40349  fourierdlem42  40366  fourierdlem44  40368  fourierdlem53  40376  fourierdlem58  40381  fourierdlem62  40385  fourierdlem76  40399  fourierdlem88  40411  fourierdlem104  40427  etransclem41  40492  etransclem44  40495  hoiqssbllem3  40838  fmtnoinf  41448  lighneallem3  41524  lighneallem4  41527  bits0eALTV  41591  oddprmALTV  41598  0nodd  41810  2nodd  41812  lindslinindsimp1  42246