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  2853  eueq3  3665  efrirr  5594  efrn2lp  5595  epne3  7706  dif1enlem  9069  ordtypelem9  9412  cantnfp1lem3  9570  cantnflem1b  9576  cantnflem1  9579  cnfcom3lem  9593  cflim2  10154  fin23lem30  10233  isf32lem5  10248  axdc3lem4  10344  axpownd  10492  pwfseqlem3  10551  grur1  10711  genpnnp  10896  xrlttri  13038  expneg  13976  bcval5  14225  seqcoll  14371  seqcoll2  14372  hashge2el2dif  14387  fsumss  15632  fprodss  15855  oddsumodd  16301  rpdvds  16571  pcmpt  16804  prmreclem2  16829  prmreclem5  16832  prmlem0  17017  sylow1lem3  19512  sylow2blem3  19534  efgredlema  19652  gsum2d2lem  19885  simpgnideld  20013  lindsind2  21756  1stccnp  23377  kqdisj  23647  alexsubALTlem4  23965  xrhmeo  24871  minveclem3b  25355  ovolgelb  25408  volsup  25484  volsup2  25533  itg1val2  25612  itg2seq  25670  itg2cn  25691  limcnlp  25806  itgsubstlem  25982  ply1termlem  26135  radcnvlt1  26354  fsumharmonic  26949  ftalem3  27012  chpub  27158  lgsqr  27289  lgseisenlem1  27313  lgsquadlem3  27320  2sqlem8a  27363  2sqlem8  27364  2sqblem  27369  nosupbnd1lem2  27648  nosupbnd2  27655  noinfbnd1lem2  27663  noinfbnd2  27670  axtgupdim2  28449  tgdim01  28485  lnoppnhpg  28742  axcontlem2  28943  minvecolem5  30861  divnumden2  32798  qsnzr  33420  mxidlirred  33437  rprmndvdsr1  33489  resssra  33599  extdgfialglem1  33705  esum2d  34106  oddpwdc  34367  eulerpartlemsv2  34371  eulerpartlemv  34377  eulerpartlemgh  34391  signslema  34575  erdszelem7  35241  erdszelem8  35242  wsuclem  35867  knoppndvlem10  36565  knoppndvlem13  36568  nlpineqsn  37452  lindsdom  37653  ftc1anclem5  37736  cntotbnd  37835  lshpdisj  39085  lcv1  39139  atlatmstc  39417  hlatcon2  39550  4noncolr3  39551  3atlem6  39586  lplnnleat  39640  lplnexllnN  39662  lvolnleat  39681  4atlem11  39707  dalem1  39757  dalemswapyzps  39788  dalemrotps  39789  2llnma1  39885  dalawlem15  39983  4atexlemcnd  40170  ltrnel  40237  cdleme15c  40374  cdleme0nex  40388  cdleme20m  40421  cdleme43bN  40588  cdleme43dN  40590  cdlemeg46nlpq  40615  cdlemg12  40748  dihmeetcN  41400  dihjatc1  41409  dihjatcclem1  41516  lclkrlem2a  41605  lcfrlem20  41660  mapdh6aN  41833  mapdh8ab  41875  hdmap1l6a  41907  aks4d1p8d1  42176  mulltgt0d  42574  mullt0b2d  42576  sn-mullt0d  42577  fimgmcyc  42626  dffltz  42726  flt4lem5a  42744  flt4lem5b  42745  flt4lem5c  42746  flt4lem5d  42747  flt4lem5e  42748  irrapxlem1  42914  elpell14qr2  42954  elpell1qr2  42964  wepwsolem  43134  fnwe2lem2  43143  brneqtrd  45172  oddfl  45378  dstregt0  45382  xrlttri5d  45384  divlt0gt0d  45386  supxrgere  45431  supxrgelem  45435  supxrge  45436  suplesup  45437  nepnfltpnf  45440  nemnftgtmnft  45442  infrpge  45449  absimnre  45573  iccdifprioo  45615  climfveq  45766  climfveqf  45777  stoweidlem34  46131  stirlinglem5  46175  dirker2re  46189  dirkerdenne0  46190  dirkertrigeq  46198  dirkercncflem2  46201  dirkercncflem4  46203  fourierdlem54  46257  elaa2lem  46330  etransclem9  46340  sge0cl  46478  sge0repnf  46483  sge0split  46506  sge0gtfsumgt  46540  mod2addne  47463  lighneallem1  47704  lighneallem3  47706  gpg3kgrtriexlem5  48186  0nodd  48269  2nodd  48271  1neven  48337