Theorem mtbird 326

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

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

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 208

This theorem is referenced by:  eqneltrd  2860  eqnbrtrd  5097  nelrnmpt  5916  rnmptn0  6202  nsuceq0  6402  fvun1  6925  tz7.44-2  8343  oeeulem  8534  supgtoreq  9381  inflb  9400  cantnfp1lem2  9598  cantnflem1  9608  rankxpsuc  9804  cardaleph  10009  cfsuc  10177  cflim2  10183  addnidpi  10822  genpnnp  10926  supaddc  12121  supmul1  12123  nnneneg  12210  indstr2  12875  zbtwnre  12894  xrltnsym  13086  xrlttr  13089  xralrple  13155  supicclub2  13455  flltnz  13768  hashelne0d  14328  hashf1lem1  14415  swrdnd  14615  swrd0  14619  sqrtneglem  15226  rlimno1  15614  binomlem  15792  fprodn0f  15954  ruclem12  16206  dvdsle  16277  2tp1odd  16319  smu01lem  16452  rpexp  16690  oddprm  16779  pythagtriplem11  16794  pythagtriplem13  16796  pcpremul  16812  pczndvds2  16836  pc2dvds  16848  pcmpt  16861  smndex1n0mnd  18881  sgrp2nmndlem5  18898  pmtrdifellem4  19452  psgnunilem1  19466  psgnunilem2  19468  efgredlemc  19718  prmcyg  19867  ablfacrplem  20040  ablfac1eulem  20047  ablsimpgfindlem1  20082  fidomndrng  20752  islbs2  21154  frlmssuvc2  21777  1stccnp  23452  fbasfip  23858  metnrmlem1a  24849  xrhmeo  24938  bndth  24950  ioombl1lem4  25553  itg2seq  25734  dvmptdiv  25966  dgrlb  26226  dgrnznn  26237  aaliou2  26331  taylthlem2  26364  cos02pilt1  26515  dvlog2lem  26641  cxple2  26686  mumullem2  27168  chtub  27200  lgsval2lem  27295  lgsdir  27320  lgsne0  27323  lgsqr  27339  lgseisenlem1  27363  lgseisenlem2  27364  lgseisenlem4  27366  lgsquadlem1  27368  lgsquad2  27374  m1lgs  27376  2sqlem7  27412  2sqblem  27419  nosupbnd1lem1  27697  nosupbnd2  27705  noinfbnd1lem1  27712  noinfbnd2lem1  27719  noinfbnd2  27720  0elold  27927  ltmuls2  28188  pw2cut2  28479  legso  28692  lmiopp  28895  axlowdimlem6  29041  elntg2  29079  1loopgrvd0  29598  1egrvtxdg0  29605  nfrgr2v  30367  nrt2irr  30568  hmdmadj  32036  strlem1  32346  isoun  32801  expgt0b  32916  archirng  33276  rsprprmprmidl  33612  rprmdvdsprod  33624  extdgfialglem1  33883  constrcon  33965  esumrnmpt2  34259  ballotlem4  34690  signswmnd  34748  signslema  34753  bnj1417  35230  satf0n0  35613  fmlaomn0  35625  prv1n  35666  tailfb  36612  weiunfr  36702  unblimceq0  36820  unbdqndv2lem2  36823  qdiff  37694  topdifinffinlem  37716  icorempo  37720  finxpreclem6  37765  lindsadd  37987  mblfinlem4  38034  3dimlem2  39958  3dimlem3a  39959  3dimlem3OLDN  39961  3dim2  39967  3dim3  39968  lplnnle2at  40040  lplnnlelln  40042  llncvrlpln  40057  lvolnle3at  40081  lvolnlelln  40083  lvolnlelpln  40084  4atlem3  40095  lplncvrlvol  40115  dalem30  40201  dalem35  40206  lhp2at0nle  40534  4atexlemswapqr  40562  ltrncnvel  40641  trlnle  40685  cdleme35sn3a  40958  cdleme46frvlpq  41003  cdlemeg46c  41012  cdlemeg46nlpq  41016  cdleme48gfv  41036  cdlemg7fvbwN  41106  cdlemg4d  41112  cdlemg10a  41139  cdlemg12d  41145  cdlemg27b  41195  cdlemg31d  41199  dihmeetlem6  41808  dochshpsat  41953  dochexmidlem1  41959  mapdindp  42170  lspindp5  42269  dvrelog2b  42558  aks4d1p1p7  42566  aks4d1p6  42573  aks6d1c2p2  42611  aks6d1c5lem1  42628  aks6d1c7lem1  42672  aks6d1c7  42676  xppss12  42723  oexpreposd  42806  mulltgt0d  42979  mullt0b2d  42981  sn-mullt0d  42982  dffltz  43091  cmpfiiin  43153  fnwe2lem2  43503  oninfint  43688  dflim5  43781  relexpmulg  44161  relexp01min  44164  relexpxpmin  44168  cvgdvgrat  44764  difmap  45659  gtnelioc  45943  ltnelicc  45949  gtnelicc  45952  lenelioc  45988  xrgtnelicc  45990  limciccioolb  46073  limcrecl  46081  limcicciooub  46087  limclner  46101  reclimc  46103  sinaover2ne0  46318  icccncfext  46337  jumpncnp  46348  itgsincmulx  46424  stoweidlem26  46476  stoweidlem35  46485  stirlinglem5  46528  dirker2re  46542  dirkerdenne0  46543  dirkertrigeqlem3  46550  dirkertrigeq  46551  dirkercncflem1  46553  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem10  46567  fourierdlem24  46581  fourierdlem25  46582  fourierdlem42  46599  fourierdlem44  46601  fourierdlem53  46609  fourierdlem58  46614  fourierdlem62  46618  fourierdlem76  46632  fourierdlem88  46644  fourierdlem104  46660  etransclem41  46725  etransclem44  46728  hoiqssbllem3  47074  smfmbfcex  47210  fsetprcnexALT  47532  difltmodne  47818  minusmodnep2tmod  47829  modm1p1ne  47846  ichnreuop  47954  fmtnoinf  48021  lighneallem3  48092  lighneallem4  48095  bits0eALTV  48178  oddprmALTV  48185  upgrimpths  48407  gpg5nbgrvtx03starlem1  48566  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem2  48570  gpg5nbgrvtx13starlem3  48571  gpg3kgrtriexlem5  48585  gpg5edgnedg  48628  0nodd  48668  2nodd  48670  lindslinindsimp1  48955  line2ylem  49249  line2xlem  49251