Theorem mtbird 327

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

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

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 209

This theorem is referenced by:  eqneltrd  2932  eqnbrtrd  5084  nsuceq0  6271  fvun1  6754  tz7.44-2  8043  oeeulem  8227  onomeneq  8708  supgtoreq  8934  inflb  8953  cantnfp1lem2  9142  cantnflem1  9152  rankxpsuc  9311  cardaleph  9515  cfsuc  9679  cflim2  9685  addnidpi  10323  genpnnp  10427  supaddc  11608  supmul1  11610  nnneneg  11673  indstr2  12328  zbtwnre  12347  xrltnsym  12531  xrlttr  12534  xralrple  12599  supicclub2  12890  flltnz  13182  hashelne0d  13730  hashf1lem1  13814  swrdnd  14016  swrd0  14020  sqrtneglem  14626  rlimno1  15010  binomlem  15184  fprodn0f  15345  ruclem12  15594  dvdsle  15660  2tp1odd  15701  smu01lem  15834  rpexp  16064  oddprm  16147  pythagtriplem11  16162  pythagtriplem13  16164  pcpremul  16180  pczndvds2  16203  pc2dvds  16215  pcmpt  16228  smndex1n0mnd  18077  sgrp2nmndlem5  18094  pmtrdifellem4  18607  psgnunilem1  18621  psgnunilem2  18623  efgredlemc  18871  prmcyg  19014  ablfacrplem  19187  ablfac1eulem  19194  ablsimpgfindlem1  19229  islbs2  19926  fidomndrng  20080  frlmssuvc2  20939  1stccnp  22070  fbasfip  22476  metnrmlem1a  23466  xrhmeo  23550  bndth  23562  ioombl1lem4  24162  itg2seq  24343  dvmptdiv  24571  dgrlb  24826  dgrnznn  24837  aaliou2  24929  taylthlem2  24962  cos02pilt1  25111  dvlog2lem  25235  cxple2  25280  mumullem2  25757  chtub  25788  lgsval2lem  25883  lgsdir  25908  lgsne0  25911  lgsqr  25927  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem4  25954  lgsquadlem1  25956  lgsquad2  25962  m1lgs  25964  2sqlem7  26000  2sqblem  26007  legso  26385  lmiopp  26588  axlowdimlem6  26733  elntg2  26771  1loopgrvd0  27286  1egrvtxdg0  27293  nfrgr2v  28051  hmdmadj  29717  strlem1  30027  isoun  30437  archirng  30817  esumrnmpt2  31327  ballotlem4  31756  signswmnd  31827  signslema  31832  bnj1417  32313  satf0n0  32625  fmlaomn0  32637  prv1n  32678  nosupbnd1lem1  33208  nosupbnd2  33216  tailfb  33725  unblimceq0  33846  unbdqndv2lem2  33849  topdifinffinlem  34631  icorempo  34635  finxpreclem6  34680  lindsadd  34900  mblfinlem4  34947  3dimlem2  36610  3dimlem3a  36611  3dimlem3OLDN  36613  3dim2  36619  3dim3  36620  lplnnle2at  36692  lplnnlelln  36694  llncvrlpln  36709  lvolnle3at  36733  lvolnlelln  36735  lvolnlelpln  36736  4atlem3  36747  lplncvrlvol  36767  dalem30  36853  dalem35  36858  lhp2at0nle  37186  4atexlemswapqr  37214  ltrncnvel  37293  trlnle  37337  cdleme35sn3a  37610  cdleme46frvlpq  37655  cdlemeg46c  37664  cdlemeg46nlpq  37668  cdleme48gfv  37688  cdlemg7fvbwN  37758  cdlemg4d  37764  cdlemg10a  37791  cdlemg12d  37797  cdlemg27b  37847  cdlemg31d  37851  dihmeetlem6  38460  dochshpsat  38605  dochexmidlem1  38611  mapdindp  38822  lspindp5  38921  xppss12  39164  oexpreposd  39228  dffltz  39320  cmpfiiin  39343  fnwe2lem2  39700  relexpmulg  40104  relexp01min  40107  relexpxpmin  40111  cvgdvgrat  40694  nelrnmpt  41397  difmap  41519  rnmptn0  41533  gtnelioc  41814  ltnelicc  41821  gtnelicc  41824  lenelioc  41861  xrgtnelicc  41863  limciccioolb  41951  limcrecl  41959  limcicciooub  41967  limclner  41981  reclimc  41983  sinaover2ne0  42198  icccncfext  42219  jumpncnp  42230  itgsincmulx  42308  stoweidlem26  42360  stoweidlem35  42369  stirlinglem5  42412  dirker2re  42426  dirkerdenne0  42427  dirkertrigeqlem3  42434  dirkertrigeq  42435  dirkercncflem1  42437  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem10  42451  fourierdlem24  42465  fourierdlem25  42466  fourierdlem42  42483  fourierdlem44  42485  fourierdlem53  42493  fourierdlem58  42498  fourierdlem62  42502  fourierdlem76  42516  fourierdlem88  42528  fourierdlem104  42544  etransclem41  42609  etransclem44  42612  hoiqssbllem3  42955  ichnreuop  43683  fmtnoinf  43747  lighneallem3  43821  lighneallem4  43824  bits0eALTV  43894  oddprmALTV  43901  0nodd  44126  2nodd  44128  lindslinindsimp1  44561  line2ylem  44787  line2xlem  44789