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  2889  eqnbrtrd  5133  nelrnmpt  5958  rnmptn0  6246  nsuceq0  6447  fvun1  6973  tz7.44-2  8394  oeeulem  8587  supgtoreq  9431  inflb  9450  cantnfp1lem2  9648  cantnflem1  9658  rankxpsuc  9854  cardaleph  10073  cfsuc  10241  cflim2  10247  addnidpi  10886  genpnnp  10990  supaddc  12182  supmul1  12184  nnneneg  12271  indstr2  12951  zbtwnre  12970  xrltnsym  13162  xrlttr  13165  xralrple  13231  supicclub2  13531  flltnz  13844  hashelne0d  14404  hashf1lem1  14492  swrdnd  14692  swrd0  14696  sqrtneglem  15317  rlimno1  15705  binomlem  15883  fprodn0f  16045  ruclem12  16297  dvdsle  16368  2tp1odd  16410  smu01lem  16543  rpexp  16781  oddprm  16870  pythagtriplem11  16885  pythagtriplem13  16887  pcpremul  16903  pczndvds2  16927  pc2dvds  16939  pcmpt  16952  smndex1n0mnd  18974  sgrp2nmndlem5  18991  pmtrdifellem4  19549  psgnunilem1  19563  psgnunilem2  19565  efgredlemc  19815  prmcyg  19964  ablfacrplem  20137  ablfac1eulem  20144  ablsimpgfindlem1  20179  fidomndrng  20855  islbs2  21256  frlmssuvc2  21914  1stccnp  23588  fbasfip  23994  metnrmlem1a  24985  xrhmeo  25074  bndth  25086  ioombl1lem4  25689  itg2seq  25870  dvmptdiv  26102  dgrlb  26362  dgrnznn  26373  aaliou2  26470  taylthlem2  26503  cos02pilt1  26657  dvlog2lem  26783  cxple2  26828  mumullem2  27310  chtub  27342  lgsval2lem  27437  lgsdir  27462  lgsne0  27465  lgsqr  27481  lgseisenlem1  27505  lgseisenlem2  27506  lgseisenlem4  27508  lgsquadlem1  27510  lgsquad2  27516  m1lgs  27518  2sqlem7  27554  2sqblem  27561  nosupbnd1lem1  27838  nosupbnd2  27846  noinfbnd1lem1  27853  noinfbnd2lem1  27860  noinfbnd2  27861  0elold  28069  ltmuls2  28330  pw2cut2  28621  legso  28834  tgelrnpln  29016  plngrotlem2  29028  lmiopp  29069  axlowdimlem6  29238  elntg2  29276  1loopgrvd0  29795  1egrvtxdg0  29802  nfrgr2v  30564  nrt2irr  30765  hmdmadj  32233  strlem1  32543  isoun  32988  expgt0b  33102  archirng  33449  rsprprmprmidl  33757  rprmdvdsprod  33769  extdgfialglem1  34027  constrcon  34109  esumrnmpt2  34403  ballotlem4  34834  signswmnd  34889  signslema  34894  bnj1417  35374  satf0n0  35803  fmlaomn0  35815  prv1n  35856  tailfb  36811  weiunfr  36901  unblimceq0  37019  unbdqndv2lem2  37022  qdiff  37893  topdifinffinlem  37915  icorempo  37919  finxpreclem6  37964  lindsadd  38186  mblfinlem4  38233  3dimlem2  40157  3dimlem3a  40158  3dimlem3OLDN  40160  3dim2  40166  3dim3  40167  lplnnle2at  40239  lplnnlelln  40241  llncvrlpln  40256  lvolnle3at  40280  lvolnlelln  40282  lvolnlelpln  40283  4atlem3  40294  lplncvrlvol  40314  dalem30  40400  dalem35  40405  lhp2at0nle  40733  4atexlemswapqr  40761  ltrncnvel  40840  trlnle  40884  cdleme35sn3a  41157  cdleme46frvlpq  41202  cdlemeg46c  41211  cdlemeg46nlpq  41215  cdleme48gfv  41235  cdlemg7fvbwN  41305  cdlemg4d  41311  cdlemg10a  41338  cdlemg12d  41344  cdlemg27b  41394  cdlemg31d  41398  dihmeetlem6  42007  dochshpsat  42152  dochexmidlem1  42158  mapdindp  42369  lspindp5  42468  dvrelog2b  42757  aks4d1p1p7  42765  aks4d1p6  42772  aks6d1c2p2  42810  aks6d1c5lem1  42827  aks6d1c7lem1  42871  aks6d1c7  42875  xppss12  42924  oexpreposd  43007  mulltgt0d  43180  mullt0b2d  43182  sn-mullt0d  43183  dffltz  43292  cmpfiiin  43354  fnwe2lem2  43704  oninfint  43889  dflim5  43982  relexpmulg  44362  relexp01min  44365  relexpxpmin  44369  cvgdvgrat  44949  difmap  45849  gtnelioc  46133  ltnelicc  46139  gtnelicc  46142  lenelioc  46178  xrgtnelicc  46180  limciccioolb  46263  limcrecl  46271  limcicciooub  46277  limclner  46291  reclimc  46293  sinaover2ne0  46508  icccncfext  46527  jumpncnp  46538  itgsincmulx  46614  stoweidlem26  46666  stoweidlem35  46675  stirlinglem5  46718  dirker2re  46732  dirkerdenne0  46733  dirkertrigeqlem3  46740  dirkertrigeq  46741  dirkercncflem1  46743  dirkercncflem2  46744  dirkercncflem4  46746  fourierdlem10  46757  fourierdlem24  46771  fourierdlem25  46772  fourierdlem42  46789  fourierdlem44  46791  fourierdlem53  46799  fourierdlem58  46804  fourierdlem62  46808  fourierdlem76  46822  fourierdlem88  46834  fourierdlem104  46850  etransclem41  46915  etransclem44  46918  hoiqssbllem3  47264  smfmbfcex  47400  fsetprcnexALT  47722  difltmodne  48008  minusmodnep2tmod  48019  modm1p1ne  48036  ichnreuop  48144  fmtnoinf  48211  lighneallem3  48282  lighneallem4  48285  bits0eALTV  48368  oddprmALTV  48375  upgrimpths  48597  gpg5nbgrvtx03starlem1  48756  gpg5nbgrvtx03starlem2  48757  gpg5nbgrvtx03starlem3  48758  gpg5nbgrvtx13starlem1  48759  gpg5nbgrvtx13starlem2  48760  gpg5nbgrvtx13starlem3  48761  gpg3kgrtriexlem5  48775  gpg5edgnedg  48818  0nodd  48858  2nodd  48860  smprngprmrng  49027  lindslinindsimp1  49156  line2ylem  49450  line2xlem  49452