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  2880  eqnbrtrd  5122  nelrnmpt  5948  rnmptn0  6245  nsuceq0  6448  fvun1  6976  fnwe2lem3  8149  tz7.44-2  8418  oeeulem  8613  supgtoreq  9466  inflb  9485  cantnfp1lem2  9683  cantnflem1  9693  rankxpsuc  9902  cardaleph  10171  cfsuc  10338  cflim2  10344  addnidpi  10989  genpnnp  11093  supaddc  12287  supmul1  12289  nnneneg  12376  indstr2  13057  zbtwnre  13076  xrltnsym  13269  xrlttr  13272  xralrple  13338  supicclub2  13638  flltnz  13954  hashelne0d  14515  hashf1lem1  14603  swrdnd  14808  swrd0  14812  sqrtneglem  15438  rlimno1  15826  binomlem  16003  fprodn0f  16163  ruclem12  16414  dvdsle  16485  2tp1odd  16527  smu01lem  16660  rpexp  16903  oddprm  16993  pythagtriplem11  17008  pythagtriplem13  17010  pcpremul  17026  pczndvds2  17050  pc2dvds  17062  pcmpt  17075  smndex1n0mnd  19116  sgrp2nmndlem5  19133  pmtrdifellem4  19698  psgnunilem1  19712  psgnunilem2  19714  efgredlemc  19964  prmcyg  20113  ablfacrplem  20286  ablfac1eulem  20293  ablsimpgfindlem1  20328  fidomndrng  21036  islbs2  21437  frlmssuvc2  22106  1stccnp  23786  fbasfip  24192  metnrmlem1a  25183  xrhmeo  25272  bndth  25284  ioombl1lem4  25887  itg2seq  26068  dvmptdiv  26299  dgrlb  26560  dgrnznn  26571  aaliou2  26672  taylthlem2  26706  cos02pilt1  26859  dvlog2lem  26985  cxple2  27030  mumullem2  27512  chtub  27544  lgsval2lem  27639  lgsdir  27664  lgsne0  27667  lgsqr  27683  lgseisenlem1  27707  lgseisenlem2  27708  lgseisenlem4  27710  lgsquadlem1  27712  lgsquad2  27718  m1lgs  27720  2sqlem7  27756  2sqblem  27763  flt4ALT  27997  nosupbnd1lem1  28070  nosupbnd2  28078  noinfbnd1lem1  28085  noinfbnd2lem1  28092  noinfbnd2  28093  0elold  28301  ltmuls2  28562  pw2cut2  28853  legso  29067  tgelrnpln  29259  plngrotlem2  29271  lmiopp  29313  axlowdimlem6  29530  elntg2  29568  1loopgrvd0  30090  1egrvtxdg0  30097  nfrgr2v  30878  nrt2irr  31079  hmdmadj  32547  strlem1  32857  isoun  33342  expgt0b  33454  archirng  33795  rsprprmprmidl  34100  rprmdvdsprod  34112  extdgfialglem1  34370  constrcon  34452  esumrnmpt2  34746  ballotlem4  35177  signswmnd  35232  signslema  35237  bnj1417  35717  acwer1prc  35816  maxssj0  35945  satf0n0  36229  fmlaomn0  36241  prv1n  36282  tailfb  37257  weiunfr  37347  unblimceq0  37465  unbdqndv2lem2  37468  qdiff  38341  topdifinffinlem  38363  icorempo  38367  finxpreclem6  38412  lindsadd  38629  mblfinlem4  38671  3dimlem2  40609  3dimlem3a  40610  3dimlem3OLDN  40612  3dim2  40618  3dim3  40619  lplnnle2at  40691  lplnnlelln  40693  llncvrlpln  40708  lvolnle3at  40732  lvolnlelln  40734  lvolnlelpln  40735  4atlem3  40746  lplncvrlvol  40766  dalem30  40852  dalem35  40857  lhp2at0nle  41185  4atexlemswapqr  41213  ltrncnvel  41292  trlnle  41336  cdleme35sn3a  41609  cdleme46frvlpq  41654  cdlemeg46c  41663  cdlemeg46nlpq  41667  cdleme48gfv  41687  cdlemg7fvbwN  41757  cdlemg4d  41763  cdlemg10a  41790  cdlemg12d  41796  cdlemg27b  41846  cdlemg31d  41850  dihmeetlem6  42459  dochshpsat  42604  dochexmidlem1  42610  mapdindp  42821  lspindp5  42920  dvrelog2b  43209  aks4d1p1p7  43217  aks4d1p6  43224  aks6d1c2p2  43262  aks6d1c5lem1  43279  aks6d1c7lem1  43323  aks6d1c7  43327  xppss12  43376  oexpreposd  43472  mulltgt0d  43639  mullt0b2d  43641  sn-mullt0d  43642  dffltz  43763  cmpfiiin  43801  oninfint  44331  dflim5  44424  relexpmulg  44803  relexp01min  44806  relexpxpmin  44810  cvgdvgrat  45390  difmap  46313  gtnelioc  46596  ltnelicc  46602  gtnelicc  46605  lenelioc  46641  xrgtnelicc  46643  limciccioolb  46726  limcrecl  46734  limcicciooub  46740  limclner  46754  reclimc  46756  sinaover2ne0  46971  icccncfext  46990  jumpncnp  47001  itgsincmulx  47077  stoweidlem26  47129  stoweidlem35  47138  stirlinglem5  47181  dirker2re  47195  dirkerdenne0  47196  dirkertrigeqlem3  47203  dirkertrigeq  47204  dirkercncflem1  47206  dirkercncflem2  47207  dirkercncflem4  47209  fourierdlem10  47220  fourierdlem24  47234  fourierdlem25  47235  fourierdlem42  47252  fourierdlem44  47254  fourierdlem53  47262  fourierdlem58  47267  fourierdlem62  47271  fourierdlem76  47285  fourierdlem88  47297  fourierdlem104  47313  etransclem41  47378  etransclem44  47381  hoiqssbllem3  47727  smfmbfcex  47863  fsetprcnexALT  48225  difltmodne  48511  minusmodnep2tmod  48522  modm1p1ne  48539  ichnreuop  48647  fmtnoinf  48714  lighneallem3  48785  lighneallem4  48788  bits0eALTV  48871  oddprmALTV  48878  upgrimpths  49100  gpg5nbgrvtx03starlem1  49259  gpg5nbgrvtx03starlem2  49260  gpg5nbgrvtx03starlem3  49261  gpg5nbgrvtx13starlem1  49262  gpg5nbgrvtx13starlem2  49263  gpg5nbgrvtx13starlem3  49264  gpg3kgrtriexlem5  49278  gpg5edgnedg  49321  0nodd  49360  2nodd  49362  smprngprmrng  49529  lindslinindsimp1  49662  line2ylem  49956  line2xlem  49958  nellindf  51138  veroquaddetzerod  51154