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  2884  eqnbrtrd  5126  nelrnmpt  5956  rnmptn0  6258  nsuceq0  6466  fvun1  6999  fnwe2lem3  8174  tz7.44-2  8443  oeeulem  8638  supgtoreq  9490  inflb  9509  cantnfp1lem2  9707  cantnflem1  9717  rankxpsuc  9926  cardaleph  10195  cfsuc  10362  cflim2  10368  addnidpi  11013  genpnnp  11117  supaddc  12311  supmul1  12313  nnneneg  12400  indstr2  13081  zbtwnre  13100  xrltnsym  13293  xrlttr  13296  xralrple  13362  supicclub2  13662  flltnz  13978  hashelne0d  14539  hashf1lem1  14627  swrdnd  14832  swrd0  14836  sqrtneglem  15462  rlimno1  15850  binomlem  16027  fprodn0f  16187  ruclem12  16438  dvdsle  16509  2tp1odd  16551  smu01lem  16684  rpexp  16927  oddprm  17017  pythagtriplem11  17032  pythagtriplem13  17034  pcpremul  17050  pczndvds2  17074  pc2dvds  17086  pcmpt  17099  smndex1n0mnd  19140  sgrp2nmndlem5  19157  pmtrdifellem4  19723  psgnunilem1  19737  psgnunilem2  19739  efgredlemc  19989  prmcyg  20138  ablfacrplem  20311  ablfac1eulem  20318  ablsimpgfindlem1  20353  fidomndrng  21061  islbs2  21462  frlmssuvc2  22131  1stccnp  23811  fbasfip  24217  metnrmlem1a  25208  xrhmeo  25297  bndth  25309  ioombl1lem4  25912  itg2seq  26093  dvmptdiv  26324  dgrlb  26585  dgrnznn  26596  aaliou2  26697  taylthlem2  26731  cos02pilt1  26884  dvlog2lem  27010  cxple2  27055  mumullem2  27537  chtub  27569  lgsval2lem  27664  lgsdir  27689  lgsne0  27692  lgsqr  27708  lgseisenlem1  27732  lgseisenlem2  27733  lgseisenlem4  27735  lgsquadlem1  27737  lgsquad2  27743  m1lgs  27745  2sqlem7  27781  2sqblem  27788  flt4ALT  28022  nosupbnd1lem1  28095  nosupbnd2  28103  noinfbnd1lem1  28110  noinfbnd2lem1  28117  noinfbnd2  28118  0elold  28326  ltmuls2  28587  pw2cut2  28878  legso  29092  tgelrnpln  29284  plngrotlem2  29296  lmiopp  29338  axlowdimlem6  29555  elntg2  29593  1loopgrvd0  30115  1egrvtxdg0  30122  nfrgr2v  30903  nrt2irr  31104  hmdmadj  32572  strlem1  32882  isoun  33366  expgt0b  33478  archirng  33819  rsprprmprmidl  34124  rprmdvdsprod  34136  extdgfialglem1  34394  constrcon  34476  esumrnmpt2  34770  ballotlem4  35201  signswmnd  35256  signslema  35261  bnj1417  35741  acwer1prc  35852  maxssj0  36006  satf0n0  36310  fmlaomn0  36322  prv1n  36363  tailfb  37343  weiunfr  37433  unblimceq0  37551  unbdqndv2lem2  37554  qdiff  38440  topdifinffinlem  38462  icorempo  38466  finxpreclem6  38511  lindsadd  38728  mblfinlem4  38770  3dimlem2  40708  3dimlem3a  40709  3dimlem3OLDN  40711  3dim2  40717  3dim3  40718  lplnnle2at  40790  lplnnlelln  40792  llncvrlpln  40807  lvolnle3at  40831  lvolnlelln  40833  lvolnlelpln  40834  4atlem3  40845  lplncvrlvol  40865  dalem30  40951  dalem35  40956  lhp2at0nle  41284  4atexlemswapqr  41312  ltrncnvel  41391  trlnle  41435  cdleme35sn3a  41708  cdleme46frvlpq  41753  cdlemeg46c  41762  cdlemeg46nlpq  41766  cdleme48gfv  41786  cdlemg7fvbwN  41856  cdlemg4d  41862  cdlemg10a  41889  cdlemg12d  41895  cdlemg27b  41945  cdlemg31d  41949  dihmeetlem6  42558  dochshpsat  42703  dochexmidlem1  42709  mapdindp  42920  lspindp5  43019  dvrelog2b  43308  aks4d1p1p7  43316  aks4d1p6  43323  aks6d1c2p2  43361  aks6d1c5lem1  43378  aks6d1c7lem1  43422  aks6d1c7  43426  xppss12  43476  oexpreposd  43572  mulltgt0d  43739  mullt0b2d  43741  sn-mullt0d  43742  dffltz  43863  cmpfiiin  43901  oninfint  44430  dflim5  44523  relexpmulg  44902  relexp01min  44905  relexpxpmin  44909  cvgdvgrat  45489  difmap  46425  gtnelioc  46708  ltnelicc  46714  gtnelicc  46717  lenelioc  46753  xrgtnelicc  46755  limciccioolb  46838  limcrecl  46846  limcicciooub  46852  limclner  46866  reclimc  46868  sinaover2ne0  47083  icccncfext  47102  jumpncnp  47113  itgsincmulx  47189  stoweidlem26  47241  stoweidlem35  47250  stirlinglem5  47293  dirker2re  47307  dirkerdenne0  47308  dirkertrigeqlem3  47315  dirkertrigeq  47316  dirkercncflem1  47318  dirkercncflem2  47319  dirkercncflem4  47321  fourierdlem10  47332  fourierdlem24  47346  fourierdlem25  47347  fourierdlem42  47364  fourierdlem44  47366  fourierdlem53  47374  fourierdlem58  47379  fourierdlem62  47383  fourierdlem76  47397  fourierdlem88  47409  fourierdlem104  47425  etransclem41  47490  etransclem44  47493  hoiqssbllem3  47839  smfmbfcex  47975  fsetprcnexALT  48337  difltmodne  48623  minusmodnep2tmod  48634  modm1p1ne  48651  ichnreuop  48759  fmtnoinf  48826  lighneallem3  48897  lighneallem4  48900  bits0eALTV  48983  oddprmALTV  48990  upgrimpths  49212  gpg5nbgrvtx03starlem1  49371  gpg5nbgrvtx03starlem2  49372  gpg5nbgrvtx03starlem3  49373  gpg5nbgrvtx13starlem1  49374  gpg5nbgrvtx13starlem2  49375  gpg5nbgrvtx13starlem3  49376  gpg3kgrtriexlem5  49390  gpg5edgnedg  49433  0nodd  49472  2nodd  49474  smprngprmrng  49641  lindslinindsimp1  49774  line2ylem  50068  line2xlem  50070  nellindf  51250  veroquaddetzerod  51266