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  2859  eueq3  3658  efrirr  5606  efrn2lp  5607  epne3  7722  dif1enlem  9089  ordtypelem9  9436  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  21813  1stccnp  23441  kqdisj  23711  alexsubALTlem4  24029  xrhmeo  24927  minveclem3b  25409  ovolgelb  25461  volsup  25537  volsup2  25586  itg1val2  25665  itg2seq  25723  itg2cn  25744  limcnlp  25859  itgsubstlem  26029  ply1termlem  26182  radcnvlt1  26400  fsumharmonic  26993  ftalem3  27056  chpub  27201  lgsqr  27332  lgseisenlem1  27356  lgsquadlem3  27363  2sqlem8a  27406  2sqlem8  27407  2sqblem  27412  nosupbnd1lem2  27691  nosupbnd2  27698  noinfbnd1lem2  27706  noinfbnd2  27713  axtgupdim2  28557  tgdim01  28593  lnoppnhpg  28850  axcontlem2  29052  minvecolem5  30971  divnumden2  32908  qsnzr  33534  mxidlirred  33551  rprmndvdsr1  33603  esplyind  33738  resssra  33750  extdgfialglem1  33856  esum2d  34257  oddpwdc  34518  eulerpartlemsv2  34522  eulerpartlemv  34528  eulerpartlemgh  34542  signslema  34726  erdszelem7  35399  erdszelem8  35400  wsuclem  36025  knoppndvlem10  36801  knoppndvlem13  36804  nlpineqsn  37744  lindsdom  37955  ftc1anclem5  38038  cntotbnd  38137  lshpdisj  39453  lcv1  39507  atlatmstc  39785  hlatcon2  39918  4noncolr3  39919  3atlem6  39954  lplnnleat  40008  lplnexllnN  40030  lvolnleat  40049  4atlem11  40075  dalem1  40125  dalemswapyzps  40156  dalemrotps  40157  2llnma1  40253  dalawlem15  40351  4atexlemcnd  40538  ltrnel  40605  cdleme15c  40742  cdleme0nex  40756  cdleme20m  40789  cdleme43bN  40956  cdleme43dN  40958  cdlemeg46nlpq  40983  cdlemg12  41116  dihmeetcN  41768  dihjatc1  41777  dihjatcclem1  41884  lclkrlem2a  41973  lcfrlem20  42028  mapdh6aN  42201  mapdh8ab  42243  hdmap1l6a  42275  aks4d1p8d1  42543  mulltgt0d  42947  mullt0b2d  42949  sn-mullt0d  42950  fimgmcyc  42999  dffltz  43087  flt4lem5a  43105  flt4lem5b  43106  flt4lem5c  43107  flt4lem5d  43108  flt4lem5e  43109  irrapxlem1  43274  elpell14qr2  43314  elpell1qr2  43324  wepwsolem  43494  fnwe2lem2  43503  brneqtrd  45531  oddfl  45735  dstregt0  45739  xrlttri5d  45741  divlt0gt0d  45743  supxrgere  45787  supxrgelem  45791  supxrge  45792  suplesup  45793  nepnfltpnf  45796  nemnftgtmnft  45798  infrpge  45805  absimnre  45928  iccdifprioo  45970  climfveq  46121  climfveqf  46132  stoweidlem34  46486  stirlinglem5  46530  dirker2re  46544  dirkerdenne0  46545  dirkertrigeq  46553  dirkercncflem2  46556  dirkercncflem4  46558  fourierdlem54  46612  elaa2lem  46685  etransclem9  46695  sge0cl  46833  sge0repnf  46838  sge0split  46861  sge0gtfsumgt  46895  mod2addne  47836  lighneallem1  48086  lighneallem3  48088  gpg3kgrtriexlem5  48581  0nodd  48664  2nodd  48666  1neven  48732