Theorem mtbird 314

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

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

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 196

This theorem is referenced by:  eqneltrd  2707  nelsnOLD  4160  eqnbrtrd  4601  nsuceq0  5722  fvun1  6179  tz7.44-2  7390  oeeulem  7568  onomeneq  8035  supgtoreq  8259  inflb  8278  cantnfp1lem2  8459  cantnflem1  8469  rankxpsuc  8628  cardaleph  8795  cfsuc  8962  cflim2  8968  addnidpi  9602  genpnnp  9706  supaddc  10867  supmul1  10869  indstr2  11643  zbtwnre  11662  xrltnsym  11846  xrlttr  11849  xralrple  11910  supicclub2  12194  flltnz  12474  hashf1lem1  13096  swrdnd  13284  swrd0  13286  sqrtneglem  13855  rlimno1  14232  binomlem  14400  fprodn0f  14561  ruclem12  14809  dvdsle  14870  2tp1odd  14914  smu01lem  15045  rpexp  15270  oddprm  15353  pythagtriplem11  15368  pythagtriplem13  15370  pcpremul  15386  pczndvds  15407  pczndvds2  15409  pc2dvds  15421  pcadd  15431  pcmpt  15434  sgrp2nmndlem5  17239  pmtrdifellem4  17722  psgnunilem1  17736  psgnunilem2  17738  efgredlemc  17981  prmcyg  18118  ablfacrplem  18287  ablfac1eulem  18294  islbs2  18975  fidomndrng  19128  frlmssuvc2  19953  1stccnp  21075  fbasfip  21482  recld2  22425  metnrmlem1a  22469  xrhmeo  22553  bndth  22565  ioombl1lem4  23136  itg2seq  23315  itg2cnlem2  23335  dgrub  23794  dgrlb  23796  dgrnznn  23807  aaliou2  23899  taylthlem2  23932  dvlog2lem  24198  cxple2  24243  mumullem2  24706  chtub  24737  lgsval2lem  24832  lgsdir  24857  lgsne0  24860  lgsqr  24876  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem4  24903  lgsquadlem1  24905  lgsquad2  24911  m1lgs  24913  2sqlem7  24949  2sqblem  24956  legso  25294  mirbtwnhl  25375  lmiopp  25494  axlowdimlem6  25627  usgra1v  25919  nbgranself  25963  cyclnspth  26159  eupath2lem3  26506  frgra2v  26526  frgrancvvdeqlem1  26557  2spotiundisj  26589  hmdmadj  28183  strlem1  28493  isoun  28862  archirng  29073  esumrnmpt2  29457  ballotlem4  29887  signswmnd  29960  signslema  29965  bnj1417  30363  tailfb  31542  unblimceq0  31668  unbdqndv2lem2  31671  topdifinffinlem  32371  icorempt2  32375  finxpreclem6  32409  mblfinlem4  32619  3dimlem2  33763  3dimlem3a  33764  3dimlem3OLDN  33766  3dim2  33772  3dim3  33773  lplnnle2at  33845  lplnnlelln  33847  llncvrlpln  33862  lvolnle3at  33886  lvolnlelln  33888  lvolnlelpln  33889  4atlem3  33900  lplncvrlvol  33920  dalem30  34006  dalem35  34011  lhp2at0nle  34339  4atexlemswapqr  34367  ltrncnvel  34446  trlnle  34491  cdleme35sn3a  34765  cdleme46frvlpq  34810  cdlemeg46c  34819  cdlemeg46nlpq  34823  cdleme48gfv  34843  cdlemg7fvbwN  34913  cdlemg4d  34919  cdlemg10a  34946  cdlemg12d  34952  cdlemg27b  35002  cdlemg31d  35006  dihmeetlem6  35616  dochshpsat  35761  dochexmidlem1  35767  mapdindp  35978  lspindp5  36077  cmpfiiin  36278  fnwe2lem2  36639  relexpmulg  37021  relexp01min  37024  relexpxpmin  37028  cvgdvgrat  37534  nelrnmpt  38283  difmap  38394  rnmptn0  38408  gtnelioc  38559  ltnelicc  38566  gtnelicc  38569  lenelioc  38610  xrgtnelicc  38612  limciccioolb  38688  limcrecl  38696  limcicciooub  38704  limclner  38718  reclimc  38720  sinaover2ne0  38751  icccncfext  38773  jumpncnp  38784  dvmptdiv  38807  itgsincmulx  38866  stoweidlem26  38919  stoweidlem35  38928  stirlinglem5  38971  dirker2re  38985  dirkerdenne0  38986  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem10  39010  fourierdlem24  39024  fourierdlem25  39025  fourierdlem42  39042  fourierdlem44  39044  fourierdlem53  39052  fourierdlem58  39057  fourierdlem62  39061  fourierdlem76  39075  fourierdlem88  39087  fourierdlem104  39103  etransclem41  39168  etransclem44  39171  hoiqssbllem3  39514  fmtnoinf  39986  lighneallem3  40062  lighneallem4  40065  bits0eALTV  40129  oddprmALTV  40136  1loopgrvd0  40719  1egrvtxdg0  40727  nfrgr2v  41442  frgrncvvdeqlem1  41469  0nodd  41600  2nodd  41602  lindslinindsimp1  42040