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 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  eqneltrd  2881  eqnbrtrd  5123  nelrnmpt  5949  rnmptn0  6238  nsuceq0  6441  fvun1  6968  tz7.44-2  8399  oeeulem  8594  supgtoreq  9447  inflb  9466  cantnfp1lem2  9664  cantnflem1  9674  rankxpsuc  9880  cardaleph  10149  cfsuc  10316  cflim2  10322  addnidpi  10967  genpnnp  11071  supaddc  12265  supmul1  12267  nnneneg  12354  indstr2  13035  zbtwnre  13054  xrltnsym  13247  xrlttr  13250  xralrple  13316  supicclub2  13616  flltnz  13931  hashelne0d  14492  hashf1lem1  14580  swrdnd  14784  swrd0  14788  sqrtneglem  15413  rlimno1  15801  binomlem  15978  fprodn0f  16138  ruclem12  16389  dvdsle  16460  2tp1odd  16502  smu01lem  16635  rpexp  16878  oddprm  16968  pythagtriplem11  16983  pythagtriplem13  16985  pcpremul  17001  pczndvds2  17025  pc2dvds  17037  pcmpt  17050  smndex1n0mnd  19091  sgrp2nmndlem5  19108  pmtrdifellem4  19673  psgnunilem1  19687  psgnunilem2  19689  efgredlemc  19939  prmcyg  20088  ablfacrplem  20261  ablfac1eulem  20268  ablsimpgfindlem1  20303  fidomndrng  21011  islbs2  21412  frlmssuvc2  22081  1stccnp  23761  fbasfip  24167  metnrmlem1a  25158  xrhmeo  25247  bndth  25259  ioombl1lem4  25862  itg2seq  26043  dvmptdiv  26274  dgrlb  26535  dgrnznn  26546  aaliou2  26649  taylthlem2  26683  cos02pilt1  26836  dvlog2lem  26962  cxple2  27007  mumullem2  27489  chtub  27521  lgsval2lem  27616  lgsdir  27641  lgsne0  27644  lgsqr  27660  lgseisenlem1  27684  lgseisenlem2  27685  lgseisenlem4  27687  lgsquadlem1  27689  lgsquad2  27695  m1lgs  27697  2sqlem7  27733  2sqblem  27740  flt4ALT  27974  nosupbnd1lem1  28047  nosupbnd2  28055  noinfbnd1lem1  28062  noinfbnd2lem1  28069  noinfbnd2  28070  0elold  28278  ltmuls2  28539  pw2cut2  28830  legso  29044  tgelrnpln  29236  plngrotlem2  29248  lmiopp  29290  axlowdimlem6  29507  elntg2  29545  1loopgrvd0  30067  1egrvtxdg0  30074  nfrgr2v  30855  nrt2irr  31056  hmdmadj  32524  strlem1  32834  isoun  33277  expgt0b  33390  archirng  33731  rsprprmprmidl  34036  rprmdvdsprod  34048  extdgfialglem1  34306  constrcon  34388  esumrnmpt2  34682  ballotlem4  35114  signswmnd  35169  signslema  35174  bnj1417  35654  satf0n0  36112  fmlaomn0  36124  prv1n  36165  tailfb  37135  weiunfr  37225  unblimceq0  37343  unbdqndv2lem2  37346  qdiff  38216  topdifinffinlem  38238  icorempo  38242  finxpreclem6  38287  lindsadd  38504  mblfinlem4  38546  3dimlem2  40484  3dimlem3a  40485  3dimlem3OLDN  40487  3dim2  40493  3dim3  40494  lplnnle2at  40566  lplnnlelln  40568  llncvrlpln  40583  lvolnle3at  40607  lvolnlelln  40609  lvolnlelpln  40610  4atlem3  40621  lplncvrlvol  40641  dalem30  40727  dalem35  40732  lhp2at0nle  41060  4atexlemswapqr  41088  ltrncnvel  41167  trlnle  41211  cdleme35sn3a  41484  cdleme46frvlpq  41529  cdlemeg46c  41538  cdlemeg46nlpq  41542  cdleme48gfv  41562  cdlemg7fvbwN  41632  cdlemg4d  41638  cdlemg10a  41665  cdlemg12d  41671  cdlemg27b  41721  cdlemg31d  41725  dihmeetlem6  42334  dochshpsat  42479  dochexmidlem1  42485  mapdindp  42696  lspindp5  42795  dvrelog2b  43084  aks4d1p1p7  43092  aks4d1p6  43099  aks6d1c2p2  43137  aks6d1c5lem1  43154  aks6d1c7lem1  43198  aks6d1c7  43202  xppss12  43251  oexpreposd  43347  mulltgt0d  43514  mullt0b2d  43516  sn-mullt0d  43517  dffltz  43624  cmpfiiin  43661  fnwe2lem2  44011  oninfint  44196  dflim5  44289  relexpmulg  44669  relexp01min  44672  relexpxpmin  44676  cvgdvgrat  45256  difmap  46163  gtnelioc  46447  ltnelicc  46453  gtnelicc  46456  lenelioc  46492  xrgtnelicc  46494  limciccioolb  46577  limcrecl  46585  limcicciooub  46591  limclner  46605  reclimc  46607  sinaover2ne0  46822  icccncfext  46841  jumpncnp  46852  itgsincmulx  46928  stoweidlem26  46980  stoweidlem35  46989  stirlinglem5  47032  dirker2re  47046  dirkerdenne0  47047  dirkertrigeqlem3  47054  dirkertrigeq  47055  dirkercncflem1  47057  dirkercncflem2  47058  dirkercncflem4  47060  fourierdlem10  47071  fourierdlem24  47085  fourierdlem25  47086  fourierdlem42  47103  fourierdlem44  47105  fourierdlem53  47113  fourierdlem58  47118  fourierdlem62  47122  fourierdlem76  47136  fourierdlem88  47148  fourierdlem104  47164  etransclem41  47229  etransclem44  47232  hoiqssbllem3  47578  smfmbfcex  47714  fsetprcnexALT  48076  difltmodne  48362  minusmodnep2tmod  48373  modm1p1ne  48390  ichnreuop  48498  fmtnoinf  48565  lighneallem3  48636  lighneallem4  48639  bits0eALTV  48722  oddprmALTV  48729  upgrimpths  48951  gpg5nbgrvtx03starlem1  49110  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx03starlem3  49112  gpg5nbgrvtx13starlem1  49113  gpg5nbgrvtx13starlem2  49114  gpg5nbgrvtx13starlem3  49115  gpg3kgrtriexlem5  49129  gpg5edgnedg  49172  0nodd  49211  2nodd  49213  smprngprmrng  49380  lindslinindsimp1  49513  line2ylem  49807  line2xlem  49809  nellindf  50914  veroquaddetzerod  50930