Theorem mtbid 326

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)

Hypotheses

Ref	Expression
mtbid.min	⊢ (𝜑 → ¬ 𝜓)
mtbid.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mtbid	⊢ (𝜑 → ¬ 𝜒)

Proof of Theorem mtbid

Step	Hyp	Ref	Expression
1		mtbid.min	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		mtbid.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimprd 250	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtod 200	1 ⊢ (𝜑 → ¬ 𝜒)

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

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 209

This theorem is referenced by:  neleqtrd  2863  eueq3  3654  efrirr  5601  efrn2lp  5602  epne3  7720  dif1enlem  9088  ordtypelem9  9435  cantnfp1lem3  9596  cantnflem1b  9602  cantnflem1  9605  cnfcom3lem  9619  cflim2  10180  fin23lem30  10259  isf32lem5  10274  axdc3lem4  10370  axpownd  10519  pwfseqlem3  10578  grur1  10738  genpnnp  10923  xrlttri  13085  expneg  14026  bcval5  14275  seqcoll  14421  seqcoll2  14422  hashge2el2dif  14437  fsumss  15682  fprodss  15908  oddsumodd  16354  rpdvds  16624  pcmpt  16858  prmreclem2  16883  prmreclem5  16886  prmlem0  17071  sylow1lem3  19570  sylow2blem3  19592  efgredlema  19710  gsum2d2lem  19943  simpgnideld  20071  lindsind2  21798  1stccnp  23449  kqdisj  23719  alexsubALTlem4  24037  xrhmeo  24935  minveclem3b  25417  ovolgelb  25469  volsup  25545  volsup2  25594  itg1val2  25673  itg2seq  25731  itg2cn  25752  limcnlp  25867  itgsubstlem  26037  ply1termlem  26190  radcnvlt1  26405  fsumharmonic  26997  ftalem3  27060  chpub  27205  lgsqr  27336  lgseisenlem1  27360  lgsquadlem3  27367  2sqlem8a  27410  2sqlem8  27411  2sqblem  27416  nosupbnd1lem2  27695  nosupbnd2  27702  noinfbnd1lem2  27710  noinfbnd2  27717  axtgupdim2  28561  tgdim01  28597  lnoppnhpg  28854  axcontlem2  29056  minvecolem5  30974  divnumden2  32912  qsnzr  33542  mxidlirred  33559  rprmndvdsr1  33619  esplyind  33771  resssra  33783  extdgfialglem1  33888  esum2d  34289  oddpwdc  34550  eulerpartlemsv2  34554  eulerpartlemv  34560  eulerpartlemgh  34574  signslema  34758  erdszelem7  35440  erdszelem8  35441  wsuclem  36066  knoppndvlem10  36842  knoppndvlem13  36845  nlpineqsn  37785  lindsdom  37996  ftc1anclem5  38079  cntotbnd  38178  lshpdisj  39494  lcv1  39548  atlatmstc  39826  hlatcon2  39959  4noncolr3  39960  3atlem6  39995  lplnnleat  40049  lplnexllnN  40071  lvolnleat  40090  4atlem11  40116  dalem1  40166  dalemswapyzps  40197  dalemrotps  40198  2llnma1  40294  dalawlem15  40392  4atexlemcnd  40579  ltrnel  40646  cdleme15c  40783  cdleme0nex  40797  cdleme20m  40830  cdleme43bN  40997  cdleme43dN  40999  cdlemeg46nlpq  41024  cdlemg12  41157  dihmeetcN  41809  dihjatc1  41818  dihjatcclem1  41925  lclkrlem2a  42014  lcfrlem20  42069  mapdh6aN  42242  mapdh8ab  42284  hdmap1l6a  42316  aks4d1p8d1  42584  mulltgt0d  42987  mullt0b2d  42989  sn-mullt0d  42990  fimgmcyc  43035  dffltz  43099  flt4lem5a  43117  flt4lem5b  43118  flt4lem5c  43119  flt4lem5d  43120  flt4lem5e  43121  irrapxlem1  43282  elpell14qr2  43322  elpell1qr2  43332  wepwsolem  43502  fnwe2lem2  43511  brneqtrd  45539  oddfl  45740  dstregt0  45744  xrlttri5d  45746  divlt0gt0d  45748  supxrgere  45792  supxrgelem  45796  supxrge  45797  suplesup  45798  nepnfltpnf  45801  nemnftgtmnft  45803  infrpge  45810  absimnre  45933  iccdifprioo  45975  climfveq  46126  climfveqf  46137  stoweidlem34  46491  stirlinglem5  46535  dirker2re  46549  dirkerdenne0  46550  dirkertrigeq  46558  dirkercncflem2  46561  dirkercncflem4  46563  fourierdlem54  46617  elaa2lem  46690  etransclem9  46700  sge0cl  46838  sge0repnf  46843  sge0split  46866  sge0gtfsumgt  46900  mod2addne  47847  lighneallem1  48097  lighneallem3  48099  gpg3kgrtriexlem5  48592  0nodd  48675  2nodd  48677  1neven  48743