Theorem mtbird 325

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

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

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 207

This theorem is referenced by:  eqneltrd  2856  eqnbrtrd  5116  nelrnmpt  5916  rnmptn0  6202  nsuceq0  6402  fvun1  6925  tz7.44-2  8338  oeeulem  8529  supgtoreq  9374  inflb  9393  cantnfp1lem2  9588  cantnflem1  9598  rankxpsuc  9794  cardaleph  9999  cfsuc  10167  cflim2  10173  addnidpi  10812  genpnnp  10916  supaddc  12109  supmul1  12111  nnneneg  12180  indstr2  12840  zbtwnre  12859  xrltnsym  13051  xrlttr  13054  xralrple  13120  supicclub2  13420  flltnz  13731  hashelne0d  14291  hashf1lem1  14378  swrdnd  14578  swrd0  14582  sqrtneglem  15189  rlimno1  15577  binomlem  15752  fprodn0f  15914  ruclem12  16166  dvdsle  16237  2tp1odd  16279  smu01lem  16412  rpexp  16649  oddprm  16738  pythagtriplem11  16753  pythagtriplem13  16755  pcpremul  16771  pczndvds2  16795  pc2dvds  16807  pcmpt  16820  smndex1n0mnd  18837  sgrp2nmndlem5  18854  pmtrdifellem4  19408  psgnunilem1  19422  psgnunilem2  19424  efgredlemc  19674  prmcyg  19823  ablfacrplem  19996  ablfac1eulem  20003  ablsimpgfindlem1  20038  fidomndrng  20706  islbs2  21109  frlmssuvc2  21750  1stccnp  23406  fbasfip  23812  metnrmlem1a  24803  xrhmeo  24900  bndth  24913  ioombl1lem4  25518  itg2seq  25699  dvmptdiv  25934  dgrlb  26197  dgrnznn  26208  aaliou2  26304  taylthlem2  26338  taylthlem2OLD  26339  cos02pilt1  26491  dvlog2lem  26617  cxple2  26662  mumullem2  27146  chtub  27179  lgsval2lem  27274  lgsdir  27299  lgsne0  27302  lgsqr  27318  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem4  27345  lgsquadlem1  27347  lgsquad2  27353  m1lgs  27355  2sqlem7  27391  2sqblem  27398  nosupbnd1lem1  27676  nosupbnd2  27684  noinfbnd1lem1  27691  noinfbnd2lem1  27698  noinfbnd2  27699  0elold  27906  ltmuls2  28167  pw2cut2  28458  legso  28671  lmiopp  28874  axlowdimlem6  29020  elntg2  29058  1loopgrvd0  29578  1egrvtxdg0  29585  nfrgr2v  30347  nrt2irr  30548  hmdmadj  32015  strlem1  32325  isoun  32781  expgt0b  32897  archirng  33270  rsprprmprmidl  33603  rprmdvdsprod  33615  extdgfialglem1  33849  constrcon  33931  esumrnmpt2  34225  ballotlem4  34656  signswmnd  34714  signslema  34719  bnj1417  35197  satf0n0  35572  fmlaomn0  35584  prv1n  35625  tailfb  36571  weiunfr  36661  unblimceq0  36707  unbdqndv2lem2  36710  topdifinffinlem  37548  icorempo  37552  finxpreclem6  37597  lindsadd  37810  mblfinlem4  37857  3dimlem2  39715  3dimlem3a  39716  3dimlem3OLDN  39718  3dim2  39724  3dim3  39725  lplnnle2at  39797  lplnnlelln  39799  llncvrlpln  39814  lvolnle3at  39838  lvolnlelln  39840  lvolnlelpln  39841  4atlem3  39852  lplncvrlvol  39872  dalem30  39958  dalem35  39963  lhp2at0nle  40291  4atexlemswapqr  40319  ltrncnvel  40398  trlnle  40442  cdleme35sn3a  40715  cdleme46frvlpq  40760  cdlemeg46c  40769  cdlemeg46nlpq  40773  cdleme48gfv  40793  cdlemg7fvbwN  40863  cdlemg4d  40869  cdlemg10a  40896  cdlemg12d  40902  cdlemg27b  40952  cdlemg31d  40956  dihmeetlem6  41565  dochshpsat  41710  dochexmidlem1  41716  mapdindp  41927  lspindp5  42026  dvrelog2b  42316  aks4d1p1p7  42324  aks4d1p6  42331  aks6d1c2p2  42369  aks6d1c5lem1  42386  aks6d1c7lem1  42430  aks6d1c7  42434  xppss12  42481  oexpreposd  42573  mulltgt0d  42733  mullt0b2d  42735  sn-mullt0d  42736  dffltz  42873  cmpfiiin  42935  fnwe2lem2  43289  oninfint  43474  dflim5  43567  relexpmulg  43947  relexp01min  43950  relexpxpmin  43954  cvgdvgrat  44550  difmap  45447  gtnelioc  45733  ltnelicc  45739  gtnelicc  45742  lenelioc  45778  xrgtnelicc  45780  limciccioolb  45863  limcrecl  45871  limcicciooub  45877  limclner  45891  reclimc  45893  sinaover2ne0  46108  icccncfext  46127  jumpncnp  46138  itgsincmulx  46214  stoweidlem26  46266  stoweidlem35  46275  stirlinglem5  46318  dirker2re  46332  dirkerdenne0  46333  dirkertrigeqlem3  46340  dirkertrigeq  46341  dirkercncflem1  46343  dirkercncflem2  46344  dirkercncflem4  46346  fourierdlem10  46357  fourierdlem24  46371  fourierdlem25  46372  fourierdlem42  46389  fourierdlem44  46391  fourierdlem53  46399  fourierdlem58  46404  fourierdlem62  46408  fourierdlem76  46422  fourierdlem88  46434  fourierdlem104  46450  etransclem41  46515  etransclem44  46518  hoiqssbllem3  46864  smfmbfcex  47000  fsetprcnexALT  47304  difltmodne  47584  minusmodnep2tmod  47595  modm1p1ne  47612  ichnreuop  47714  fmtnoinf  47778  lighneallem3  47849  lighneallem4  47852  bits0eALTV  47922  oddprmALTV  47929  upgrimpths  48151  gpg5nbgrvtx03starlem1  48310  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx03starlem3  48312  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem2  48314  gpg5nbgrvtx13starlem3  48315  gpg3kgrtriexlem5  48329  gpg5edgnedg  48372  0nodd  48412  2nodd  48414  lindslinindsimp1  48699  line2ylem  48993  line2xlem  48995