Theorem mtbird 328

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

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

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 210

This theorem is referenced by:  eqneltrd  2885  eqnbrtrd  5123  nelrnmpt  5948  rnmptn0  6235  nsuceq0  6435  fvun1  6962  tz7.44-2  8382  oeeulem  8575  supgtoreq  9419  inflb  9438  cantnfp1lem2  9636  cantnflem1  9646  rankxpsuc  9842  cardaleph  10061  cfsuc  10229  cflim2  10235  addnidpi  10874  genpnnp  10978  supaddc  12173  supmul1  12175  nnneneg  12262  indstr2  12942  zbtwnre  12961  xrltnsym  13153  xrlttr  13156  xralrple  13222  supicclub2  13522  flltnz  13835  hashelne0d  14395  hashf1lem1  14482  swrdnd  14682  swrd0  14686  sqrtneglem  15307  rlimno1  15695  binomlem  15873  fprodn0f  16035  ruclem12  16287  dvdsle  16358  2tp1odd  16400  smu01lem  16533  rpexp  16771  oddprm  16860  pythagtriplem11  16875  pythagtriplem13  16877  pcpremul  16893  pczndvds2  16917  pc2dvds  16929  pcmpt  16942  smndex1n0mnd  18964  sgrp2nmndlem5  18981  pmtrdifellem4  19540  psgnunilem1  19554  psgnunilem2  19556  efgredlemc  19806  prmcyg  19955  ablfacrplem  20128  ablfac1eulem  20135  ablsimpgfindlem1  20170  fidomndrng  20846  islbs2  21247  frlmssuvc2  21905  1stccnp  23580  fbasfip  23986  metnrmlem1a  24977  xrhmeo  25066  bndth  25078  ioombl1lem4  25681  itg2seq  25862  dvmptdiv  26094  dgrlb  26354  dgrnznn  26365  aaliou2  26462  taylthlem2  26495  cos02pilt1  26649  dvlog2lem  26775  cxple2  26820  mumullem2  27302  chtub  27334  lgsval2lem  27429  lgsdir  27454  lgsne0  27457  lgsqr  27473  lgseisenlem1  27497  lgseisenlem2  27498  lgseisenlem4  27500  lgsquadlem1  27502  lgsquad2  27508  m1lgs  27510  2sqlem7  27546  2sqblem  27553  nosupbnd1lem1  27830  nosupbnd2  27838  noinfbnd1lem1  27845  noinfbnd2lem1  27852  noinfbnd2  27853  0elold  28061  ltmuls2  28322  pw2cut2  28613  legso  28826  tgelrnpln  29006  plngrotlem2  29018  lmiopp  29054  axlowdimlem6  29206  elntg2  29244  1loopgrvd0  29763  1egrvtxdg0  29770  nfrgr2v  30532  nrt2irr  30733  hmdmadj  32201  strlem1  32511  isoun  32959  expgt0b  33074  archirng  33421  rsprprmprmidl  33729  rprmdvdsprod  33741  extdgfialglem1  33999  constrcon  34081  esumrnmpt2  34375  ballotlem4  34806  signswmnd  34861  signslema  34866  bnj1417  35346  satf0n0  35741  fmlaomn0  35753  prv1n  35794  tailfb  36750  weiunfr  36840  unblimceq0  36958  unbdqndv2lem2  36961  qdiff  37831  topdifinffinlem  37853  icorempo  37857  finxpreclem6  37902  lindsadd  38124  mblfinlem4  38171  3dimlem2  40095  3dimlem3a  40096  3dimlem3OLDN  40098  3dim2  40104  3dim3  40105  lplnnle2at  40177  lplnnlelln  40179  llncvrlpln  40194  lvolnle3at  40218  lvolnlelln  40220  lvolnlelpln  40221  4atlem3  40232  lplncvrlvol  40252  dalem30  40338  dalem35  40343  lhp2at0nle  40671  4atexlemswapqr  40699  ltrncnvel  40778  trlnle  40822  cdleme35sn3a  41095  cdleme46frvlpq  41140  cdlemeg46c  41149  cdlemeg46nlpq  41153  cdleme48gfv  41173  cdlemg7fvbwN  41243  cdlemg4d  41249  cdlemg10a  41276  cdlemg12d  41282  cdlemg27b  41332  cdlemg31d  41336  dihmeetlem6  41945  dochshpsat  42090  dochexmidlem1  42096  mapdindp  42307  lspindp5  42406  dvrelog2b  42695  aks4d1p1p7  42703  aks4d1p6  42710  aks6d1c2p2  42748  aks6d1c5lem1  42765  aks6d1c7lem1  42809  aks6d1c7  42813  xppss12  42860  oexpreposd  42943  mulltgt0d  43116  mullt0b2d  43118  sn-mullt0d  43119  dffltz  43228  cmpfiiin  43290  fnwe2lem2  43640  oninfint  43825  dflim5  43918  relexpmulg  44298  relexp01min  44301  relexpxpmin  44305  cvgdvgrat  44887  difmap  45781  gtnelioc  46065  ltnelicc  46071  gtnelicc  46074  lenelioc  46110  xrgtnelicc  46112  limciccioolb  46195  limcrecl  46203  limcicciooub  46209  limclner  46223  reclimc  46225  sinaover2ne0  46440  icccncfext  46459  jumpncnp  46470  itgsincmulx  46546  stoweidlem26  46598  stoweidlem35  46607  stirlinglem5  46650  dirker2re  46664  dirkerdenne0  46665  dirkertrigeqlem3  46672  dirkertrigeq  46673  dirkercncflem1  46675  dirkercncflem2  46676  dirkercncflem4  46678  fourierdlem10  46689  fourierdlem24  46703  fourierdlem25  46704  fourierdlem42  46721  fourierdlem44  46723  fourierdlem53  46731  fourierdlem58  46736  fourierdlem62  46740  fourierdlem76  46754  fourierdlem88  46766  fourierdlem104  46782  etransclem41  46847  etransclem44  46850  hoiqssbllem3  47196  smfmbfcex  47332  fsetprcnexALT  47654  difltmodne  47940  minusmodnep2tmod  47951  modm1p1ne  47968  ichnreuop  48076  fmtnoinf  48143  lighneallem3  48214  lighneallem4  48217  bits0eALTV  48300  oddprmALTV  48307  upgrimpths  48529  gpg5nbgrvtx03starlem1  48688  gpg5nbgrvtx03starlem2  48689  gpg5nbgrvtx03starlem3  48690  gpg5nbgrvtx13starlem1  48691  gpg5nbgrvtx13starlem2  48692  gpg5nbgrvtx13starlem3  48693  gpg3kgrtriexlem5  48707  gpg5edgnedg  48750  0nodd  48790  2nodd  48792  smprngprmrng  48959  lindslinindsimp1  49088  line2ylem  49382  line2xlem  49384