Theorem mtbird 324

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

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

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 206

This theorem is referenced by:  eqneltrd  2853  eqnbrtrd  5166  rnmptn0  6243  nsuceq0  6447  fvun1  6982  tz7.44-2  8409  oeeulem  8603  onomeneqOLD  9231  supgtoreq  9467  inflb  9486  cantnfp1lem2  9676  cantnflem1  9686  rankxpsuc  9879  cardaleph  10086  cfsuc  10254  cflim2  10260  addnidpi  10898  genpnnp  11002  supaddc  12185  supmul1  12187  nnneneg  12251  indstr2  12915  zbtwnre  12934  xrltnsym  13120  xrlttr  13123  xralrple  13188  supicclub2  13485  flltnz  13780  hashelne0d  14332  hashf1lem1  14419  hashf1lem1OLD  14420  swrdnd  14608  swrd0  14612  sqrtneglem  15217  rlimno1  15604  binomlem  15779  fprodn0f  15939  ruclem12  16188  dvdsle  16257  2tp1odd  16299  smu01lem  16430  rpexp  16663  oddprm  16747  pythagtriplem11  16762  pythagtriplem13  16764  pcpremul  16780  pczndvds2  16804  pc2dvds  16816  pcmpt  16829  smndex1n0mnd  18829  sgrp2nmndlem5  18846  pmtrdifellem4  19388  psgnunilem1  19402  psgnunilem2  19404  efgredlemc  19654  prmcyg  19803  ablfacrplem  19976  ablfac1eulem  19983  ablsimpgfindlem1  20018  islbs2  20912  fidomndrng  21126  frlmssuvc2  21569  1stccnp  23186  fbasfip  23592  metnrmlem1a  24594  xrhmeo  24686  bndth  24698  ioombl1lem4  25302  itg2seq  25484  dvmptdiv  25715  dgrlb  25974  dgrnznn  25985  aaliou2  26077  taylthlem2  26110  cos02pilt1  26259  dvlog2lem  26384  cxple2  26429  mumullem2  26908  chtub  26939  lgsval2lem  27034  lgsdir  27059  lgsne0  27062  lgsqr  27078  lgseisenlem1  27102  lgseisenlem2  27103  lgseisenlem4  27105  lgsquadlem1  27107  lgsquad2  27113  m1lgs  27115  2sqlem7  27151  2sqblem  27158  nosupbnd1lem1  27435  nosupbnd2  27443  noinfbnd1lem1  27450  noinfbnd2lem1  27457  noinfbnd2  27458  0elold  27628  sltmul2  27850  legso  28105  lmiopp  28308  axlowdimlem6  28460  elntg2  28498  1loopgrvd0  29016  1egrvtxdg0  29023  nfrgr2v  29780  nrt2irr  29981  hmdmadj  31448  strlem1  31758  isoun  32178  archirng  32592  esumrnmpt2  33352  ballotlem4  33783  signswmnd  33854  signslema  33859  bnj1417  34338  satf0n0  34655  fmlaomn0  34667  prv1n  34708  tailfb  35565  unblimceq0  35686  unbdqndv2lem2  35689  topdifinffinlem  36531  icorempo  36535  finxpreclem6  36580  lindsadd  36784  mblfinlem4  36831  3dimlem2  38633  3dimlem3a  38634  3dimlem3OLDN  38636  3dim2  38642  3dim3  38643  lplnnle2at  38715  lplnnlelln  38717  llncvrlpln  38732  lvolnle3at  38756  lvolnlelln  38758  lvolnlelpln  38759  4atlem3  38770  lplncvrlvol  38790  dalem30  38876  dalem35  38881  lhp2at0nle  39209  4atexlemswapqr  39237  ltrncnvel  39316  trlnle  39360  cdleme35sn3a  39633  cdleme46frvlpq  39678  cdlemeg46c  39687  cdlemeg46nlpq  39691  cdleme48gfv  39711  cdlemg7fvbwN  39781  cdlemg4d  39787  cdlemg10a  39814  cdlemg12d  39820  cdlemg27b  39870  cdlemg31d  39874  dihmeetlem6  40483  dochshpsat  40628  dochexmidlem1  40634  mapdindp  40845  lspindp5  40944  dvrelog2b  41237  aks4d1p1p7  41245  aks4d1p6  41252  aks6d1c2p2  41263  metakunt30  41320  xppss12  41353  oexpreposd  41514  dffltz  41678  cmpfiiin  41737  fnwe2lem2  42095  oninfint  42287  dflim5  42381  relexpmulg  42763  relexp01min  42766  relexpxpmin  42770  cvgdvgrat  43374  nelrnmpt  44075  difmap  44205  gtnelioc  44503  ltnelicc  44509  gtnelicc  44512  lenelioc  44548  xrgtnelicc  44550  limciccioolb  44636  limcrecl  44644  limcicciooub  44652  limclner  44666  reclimc  44668  sinaover2ne0  44883  icccncfext  44902  jumpncnp  44913  itgsincmulx  44989  stoweidlem26  45041  stoweidlem35  45050  stirlinglem5  45093  dirker2re  45107  dirkerdenne0  45108  dirkertrigeqlem3  45115  dirkertrigeq  45116  dirkercncflem1  45118  dirkercncflem2  45119  dirkercncflem4  45121  fourierdlem10  45132  fourierdlem24  45146  fourierdlem25  45147  fourierdlem42  45164  fourierdlem44  45166  fourierdlem53  45174  fourierdlem58  45179  fourierdlem62  45183  fourierdlem76  45197  fourierdlem88  45209  fourierdlem104  45225  etransclem41  45290  etransclem44  45293  hoiqssbllem3  45639  smfmbfcex  45775  fsetprcnexALT  46071  ichnreuop  46439  fmtnoinf  46503  lighneallem3  46574  lighneallem4  46577  bits0eALTV  46647  oddprmALTV  46654  0nodd  46847  2nodd  46849  lindslinindsimp1  47226  line2ylem  47525  line2xlem  47527