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  2882  eqnbrtrd  5127  nelrnmpt  5955  rnmptn0  6244  nsuceq0  6447  fvun1  6973  tz7.44-2  8400  oeeulem  8593  supgtoreq  9445  inflb  9464  cantnfp1lem2  9662  cantnflem1  9672  rankxpsuc  9868  cardaleph  10096  cfsuc  10263  cflim2  10269  addnidpi  10914  genpnnp  11018  supaddc  12210  supmul1  12212  nnneneg  12299  indstr2  12980  zbtwnre  12999  xrltnsym  13192  xrlttr  13195  xralrple  13261  supicclub2  13561  flltnz  13876  hashelne0d  14436  hashf1lem1  14524  swrdnd  14728  swrd0  14732  sqrtneglem  15357  rlimno1  15745  binomlem  15922  fprodn0f  16084  ruclem12  16335  dvdsle  16406  2tp1odd  16448  smu01lem  16581  rpexp  16819  oddprm  16908  pythagtriplem11  16923  pythagtriplem13  16925  pcpremul  16941  pczndvds2  16965  pc2dvds  16977  pcmpt  16990  smndex1n0mnd  19030  sgrp2nmndlem5  19047  pmtrdifellem4  19612  psgnunilem1  19626  psgnunilem2  19628  efgredlemc  19878  prmcyg  20027  ablfacrplem  20200  ablfac1eulem  20207  ablsimpgfindlem1  20242  fidomndrng  20946  islbs2  21347  frlmssuvc2  22014  1stccnp  23694  fbasfip  24100  metnrmlem1a  25091  xrhmeo  25180  bndth  25192  ioombl1lem4  25795  itg2seq  25976  dvmptdiv  26208  dgrlb  26469  dgrnznn  26480  aaliou2  26583  taylthlem2  26617  cos02pilt1  26771  dvlog2lem  26897  cxple2  26942  mumullem2  27424  chtub  27456  lgsval2lem  27551  lgsdir  27576  lgsne0  27579  lgsqr  27595  lgseisenlem1  27619  lgseisenlem2  27620  lgseisenlem4  27622  lgsquadlem1  27624  lgsquad2  27630  m1lgs  27632  2sqlem7  27668  2sqblem  27675  nosupbnd1lem1  27952  nosupbnd2  27960  noinfbnd1lem1  27967  noinfbnd2lem1  27974  noinfbnd2  27975  0elold  28183  ltmuls2  28444  pw2cut2  28735  legso  28949  tgelrnpln  29141  plngrotlem2  29153  lmiopp  29195  axlowdimlem6  29412  elntg2  29450  1loopgrvd0  29972  1egrvtxdg0  29979  nfrgr2v  30760  nrt2irr  30961  hmdmadj  32429  strlem1  32739  isoun  33182  expgt0b  33295  archirng  33636  rsprprmprmidl  33940  rprmdvdsprod  33952  extdgfialglem1  34210  constrcon  34292  esumrnmpt2  34586  ballotlem4  35018  signswmnd  35073  signslema  35078  bnj1417  35558  satf0n0  35965  fmlaomn0  35977  prv1n  36018  tailfb  37004  weiunfr  37094  unblimceq0  37212  unbdqndv2lem2  37215  qdiff  38087  topdifinffinlem  38109  icorempo  38113  finxpreclem6  38158  lindsadd  38375  mblfinlem4  38417  3dimlem2  40340  3dimlem3a  40341  3dimlem3OLDN  40343  3dim2  40349  3dim3  40350  lplnnle2at  40422  lplnnlelln  40424  llncvrlpln  40439  lvolnle3at  40463  lvolnlelln  40465  lvolnlelpln  40466  4atlem3  40477  lplncvrlvol  40497  dalem30  40583  dalem35  40588  lhp2at0nle  40916  4atexlemswapqr  40944  ltrncnvel  41023  trlnle  41067  cdleme35sn3a  41340  cdleme46frvlpq  41385  cdlemeg46c  41394  cdlemeg46nlpq  41398  cdleme48gfv  41418  cdlemg7fvbwN  41488  cdlemg4d  41494  cdlemg10a  41521  cdlemg12d  41527  cdlemg27b  41577  cdlemg31d  41581  dihmeetlem6  42190  dochshpsat  42335  dochexmidlem1  42341  mapdindp  42552  lspindp5  42651  dvrelog2b  42940  aks4d1p1p7  42948  aks4d1p6  42955  aks6d1c2p2  42993  aks6d1c5lem1  43010  aks6d1c7lem1  43054  aks6d1c7  43058  xppss12  43107  oexpreposd  43205  mulltgt0d  43378  mullt0b2d  43380  sn-mullt0d  43381  dffltz  43488  cmpfiiin  43550  fnwe2lem2  43900  oninfint  44085  dflim5  44178  relexpmulg  44558  relexp01min  44561  relexpxpmin  44565  cvgdvgrat  45145  difmap  46045  gtnelioc  46329  ltnelicc  46335  gtnelicc  46338  lenelioc  46374  xrgtnelicc  46376  limciccioolb  46459  limcrecl  46467  limcicciooub  46473  limclner  46487  reclimc  46489  sinaover2ne0  46704  icccncfext  46723  jumpncnp  46734  itgsincmulx  46810  stoweidlem26  46862  stoweidlem35  46871  stirlinglem5  46914  dirker2re  46928  dirkerdenne0  46929  dirkertrigeqlem3  46936  dirkertrigeq  46937  dirkercncflem1  46939  dirkercncflem2  46940  dirkercncflem4  46942  fourierdlem10  46953  fourierdlem24  46967  fourierdlem25  46968  fourierdlem42  46985  fourierdlem44  46987  fourierdlem53  46995  fourierdlem58  47000  fourierdlem62  47004  fourierdlem76  47018  fourierdlem88  47030  fourierdlem104  47046  etransclem41  47111  etransclem44  47114  hoiqssbllem3  47460  smfmbfcex  47596  fsetprcnexALT  47958  difltmodne  48244  minusmodnep2tmod  48255  modm1p1ne  48272  ichnreuop  48380  fmtnoinf  48447  lighneallem3  48518  lighneallem4  48521  bits0eALTV  48604  oddprmALTV  48611  upgrimpths  48833  gpg5nbgrvtx03starlem1  48992  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx03starlem3  48994  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem2  48996  gpg5nbgrvtx13starlem3  48997  gpg3kgrtriexlem5  49011  gpg5edgnedg  49054  0nodd  49093  2nodd  49095  smprngprmrng  49262  lindslinindsimp1  49395  line2ylem  49689  line2xlem  49691  nellindf  50811  veroquaddetzerod  50827