Theorem mtbird 317

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

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

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 199

This theorem is referenced by:  eqneltrd  2878  eqnbrtrd  4904  nsuceq0  6056  fvun1  6529  tz7.44-2  7786  oeeulem  7965  onomeneq  8438  supgtoreq  8664  inflb  8683  cantnfp1lem2  8873  cantnflem1  8883  rankxpsuc  9042  cardaleph  9245  cfsuc  9414  cflim2  9420  addnidpi  10058  genpnnp  10162  supaddc  11344  supmul1  11346  indstr2  12074  zbtwnre  12093  xrltnsym  12280  xrlttr  12283  xralrple  12348  supicclub2  12640  flltnz  12931  hashf1lem1  13553  swrdnd  13749  swrd0  13753  sqrtneglem  14414  rlimno1  14792  binomlem  14965  fprodn0f  15124  ruclem12  15374  dvdsle  15439  2tp1odd  15480  smu01lem  15613  rpexp  15836  oddprm  15919  pythagtriplem11  15934  pythagtriplem13  15936  pcpremul  15952  pczndvds2  15975  pc2dvds  15987  pcmpt  16000  sgrp2nmndlem5  17803  pmtrdifellem4  18282  psgnunilem1  18296  psgnunilem2  18299  efgredlemc  18543  prmcyg  18681  ablfacrplem  18851  ablfac1eulem  18858  islbs2  19551  fidomndrng  19704  frlmssuvc2  20538  1stccnp  21674  fbasfip  22080  recld2  23025  metnrmlem1a  23069  xrhmeo  23153  bndth  23165  ioombl1lem4  23765  itg2seq  23946  itg2cnlem2  23966  dvmptdiv  24174  dgrub  24427  dgrlb  24429  dgrnznn  24440  aaliou2  24532  taylthlem2  24565  dvlog2lem  24835  cxple2  24880  mumullem2  25358  chtub  25389  lgsval2lem  25484  lgsdir  25509  lgsne0  25512  lgsqr  25528  lgseisenlem1  25552  lgseisenlem2  25553  lgseisenlem4  25555  lgsquadlem1  25557  lgsquad2  25563  m1lgs  25565  2sqlem7  25601  2sqblem  25608  legso  25950  mirbtwnhl  26031  lmiopp  26150  axlowdimlem6  26296  elntg2  26334  1loopgrvd0  26852  1egrvtxdg0  26859  nfrgr2v  27680  hmdmadj  29371  strlem1  29681  isoun  30045  archirng  30304  esumrnmpt2  30728  ballotlem4  31159  signswmnd  31234  signslema  31239  bnj1417  31708  nosupbnd1lem1  32443  nosupbnd2  32451  tailfb  32960  unblimceq0  33080  unbdqndv2lem2  33083  topdifinffinlem  33790  icorempt2  33794  finxpreclem6  33828  lindsadd  34030  mblfinlem4  34077  3dimlem2  35615  3dimlem3a  35616  3dimlem3OLDN  35618  3dim2  35624  3dim3  35625  lplnnle2at  35697  lplnnlelln  35699  llncvrlpln  35714  lvolnle3at  35738  lvolnlelln  35740  lvolnlelpln  35741  4atlem3  35752  lplncvrlvol  35772  dalem30  35858  dalem35  35863  lhp2at0nle  36191  4atexlemswapqr  36219  ltrncnvel  36298  trlnle  36342  cdleme35sn3a  36615  cdleme46frvlpq  36660  cdlemeg46c  36669  cdlemeg46nlpq  36673  cdleme48gfv  36693  cdlemg7fvbwN  36763  cdlemg4d  36769  cdlemg10a  36796  cdlemg12d  36802  cdlemg27b  36852  cdlemg31d  36856  dihmeetlem6  37465  dochshpsat  37610  dochexmidlem1  37616  mapdindp  37827  lspindp5  37926  xppss12  38129  oexpreposd  38161  dffltz  38217  cmpfiiin  38224  fnwe2lem2  38584  relexpmulg  38963  relexp01min  38966  relexpxpmin  38970  cvgdvgrat  39472  nelrnmpt  40192  difmap  40324  rnmptn0  40338  gtnelioc  40628  ltnelicc  40635  gtnelicc  40638  lenelioc  40675  xrgtnelicc  40677  limciccioolb  40765  limcrecl  40773  limcicciooub  40781  limclner  40795  reclimc  40797  sinaover2ne0  41011  icccncfext  41032  jumpncnp  41043  itgsincmulx  41121  stoweidlem26  41174  stoweidlem35  41183  stirlinglem5  41226  dirker2re  41240  dirkerdenne0  41241  dirkertrigeqlem3  41248  dirkertrigeq  41249  dirkercncflem1  41251  dirkercncflem2  41252  dirkercncflem4  41254  fourierdlem10  41265  fourierdlem24  41279  fourierdlem25  41280  fourierdlem42  41297  fourierdlem44  41299  fourierdlem53  41307  fourierdlem58  41312  fourierdlem62  41316  fourierdlem76  41330  fourierdlem88  41342  fourierdlem104  41358  etransclem41  41423  etransclem44  41426  hoiqssbllem3  41769  fmtnoinf  42473  lighneallem3  42549  lighneallem4  42552  bits0eALTV  42620  oddprmALTV  42627  0nodd  42829  2nodd  42831  lindslinindsimp1  43265  line2ylem  43491  line2xlem  43493