Theorem mtbid 324

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 248	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtod 198	1 ⊢ (𝜑 → ¬ 𝜒)

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

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 207

This theorem is referenced by:  neleqtrd  2850  eueq3  3679  efrirr  5611  efrn2lp  5612  epne3  7729  dif1enlem  9097  dif1enlemOLD  9098  ordtypelem9  9455  cantnfp1lem3  9609  cantnflem1b  9615  cantnflem1  9618  cnfcom3lem  9632  cflim2  10192  fin23lem30  10271  isf32lem5  10286  axdc3lem4  10382  axpownd  10530  pwfseqlem3  10589  grur1  10749  genpnnp  10934  xrlttri  13075  expneg  14010  bcval5  14259  seqcoll  14405  seqcoll2  14406  hashge2el2dif  14421  fsumss  15667  fprodss  15890  oddsumodd  16336  rpdvds  16606  pcmpt  16839  prmreclem2  16864  prmreclem5  16867  prmlem0  17052  sylow1lem3  19514  sylow2blem3  19536  efgredlema  19654  gsum2d2lem  19887  simpgnideld  20015  lindsind2  21761  1stccnp  23382  kqdisj  23652  alexsubALTlem4  23970  xrhmeo  24877  minveclem3b  25361  ovolgelb  25414  volsup  25490  volsup2  25539  itg1val2  25618  itg2seq  25676  itg2cn  25697  limcnlp  25812  itgsubstlem  25988  ply1termlem  26141  radcnvlt1  26360  fsumharmonic  26955  ftalem3  27018  chpub  27164  lgsqr  27295  lgseisenlem1  27319  lgsquadlem3  27326  2sqlem8a  27369  2sqlem8  27370  2sqblem  27375  nosupbnd1lem2  27654  nosupbnd2  27661  noinfbnd1lem2  27669  noinfbnd2  27676  axtgupdim2  28451  tgdim01  28487  lnoppnhpg  28744  axcontlem2  28945  minvecolem5  30860  divnumden2  32790  qsnzr  33419  mxidlirred  33436  rprmndvdsr1  33488  resssra  33576  esum2d  34076  oddpwdc  34338  eulerpartlemsv2  34342  eulerpartlemv  34348  eulerpartlemgh  34362  signslema  34546  erdszelem7  35177  erdszelem8  35178  wsuclem  35806  knoppndvlem10  36502  knoppndvlem13  36505  nlpineqsn  37389  lindsdom  37601  ftc1anclem5  37684  cntotbnd  37783  lshpdisj  38973  lcv1  39027  atlatmstc  39305  hlatcon2  39439  4noncolr3  39440  3atlem6  39475  lplnnleat  39529  lplnexllnN  39551  lvolnleat  39570  4atlem11  39596  dalem1  39646  dalemswapyzps  39677  dalemrotps  39678  2llnma1  39774  dalawlem15  39872  4atexlemcnd  40059  ltrnel  40126  cdleme15c  40263  cdleme0nex  40277  cdleme20m  40310  cdleme43bN  40477  cdleme43dN  40479  cdlemeg46nlpq  40504  cdlemg12  40637  dihmeetcN  41289  dihjatc1  41298  dihjatcclem1  41405  lclkrlem2a  41494  lcfrlem20  41549  mapdh6aN  41722  mapdh8ab  41764  hdmap1l6a  41796  aks4d1p8d1  42065  mulltgt0d  42463  mullt0b2d  42465  sn-mullt0d  42466  fimgmcyc  42515  dffltz  42615  flt4lem5a  42633  flt4lem5b  42634  flt4lem5c  42635  flt4lem5d  42636  flt4lem5e  42637  irrapxlem1  42803  elpell14qr2  42843  elpell1qr2  42853  wepwsolem  43024  fnwe2lem2  43033  brneqtrd  45063  oddfl  45269  dstregt0  45273  xrlttri5d  45275  divlt0gt0d  45277  supxrgere  45322  supxrgelem  45326  supxrge  45327  suplesup  45328  nepnfltpnf  45331  nemnftgtmnft  45333  infrpge  45340  absimnre  45465  iccdifprioo  45507  climfveq  45660  climfveqf  45671  stoweidlem34  46025  stirlinglem5  46069  dirker2re  46083  dirkerdenne0  46084  dirkertrigeq  46092  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem54  46151  elaa2lem  46224  etransclem9  46234  sge0cl  46372  sge0repnf  46377  sge0split  46400  sge0gtfsumgt  46434  tworepnotupword  46877  mod2addne  47358  lighneallem1  47599  lighneallem3  47601  gpg3kgrtriexlem5  48071  0nodd  48151  2nodd  48153  1neven  48219