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  2866  eueq3  3733  efrirr  5680  efrn2lp  5681  epne3  7808  wfrlem10OLD  8374  dif1enlem  9222  dif1enlemOLD  9223  ordtypelem9  9595  cantnfp1lem3  9749  cantnflem1b  9755  cantnflem1  9758  cnfcom3lem  9772  cflim2  10332  fin23lem30  10411  isf32lem5  10426  axdc3lem4  10522  axpownd  10670  pwfseqlem3  10729  grur1  10889  genpnnp  11074  xrlttri  13201  expneg  14120  bcval5  14367  seqcoll  14513  seqcoll2  14514  hashge2el2dif  14529  fsumss  15773  fprodss  15996  oddsumodd  16438  rpdvds  16707  pcmpt  16939  prmreclem2  16964  prmreclem5  16967  prmlem0  17153  sylow1lem3  19642  sylow2blem3  19664  efgredlema  19782  gsum2d2lem  20015  simpgnideld  20143  lindsind2  21862  1stccnp  23491  kqdisj  23761  alexsubALTlem4  24079  xrhmeo  24996  minveclem3b  25481  ovolgelb  25534  volsup  25610  volsup2  25659  itg1val2  25738  itg2seq  25797  itg2cn  25818  limcnlp  25933  itgsubstlem  26109  ply1termlem  26262  radcnvlt1  26479  fsumharmonic  27073  ftalem3  27136  chpub  27282  lgsqr  27413  lgseisenlem1  27437  lgsquadlem3  27444  2sqlem8a  27487  2sqlem8  27488  2sqblem  27493  nosupbnd1lem2  27772  nosupbnd2  27779  noinfbnd1lem2  27787  noinfbnd2  27794  axtgupdim2  28497  tgdim01  28533  lnoppnhpg  28790  axcontlem2  28998  minvecolem5  30913  divnumden2  32819  qsnzr  33448  mxidlirred  33465  rprmndvdsr1  33517  resssra  33602  esum2d  34057  oddpwdc  34319  eulerpartlemsv2  34323  eulerpartlemv  34329  eulerpartlemgh  34343  signslema  34539  erdszelem7  35165  erdszelem8  35166  wsuclem  35789  knoppndvlem10  36487  knoppndvlem13  36490  nlpineqsn  37374  lindsdom  37574  ftc1anclem5  37657  cntotbnd  37756  lshpdisj  38943  lcv1  38997  atlatmstc  39275  hlatcon2  39409  4noncolr3  39410  3atlem6  39445  lplnnleat  39499  lplnexllnN  39521  lvolnleat  39540  4atlem11  39566  dalem1  39616  dalemswapyzps  39647  dalemrotps  39648  2llnma1  39744  dalawlem15  39842  4atexlemcnd  40029  ltrnel  40096  cdleme15c  40233  cdleme0nex  40247  cdleme20m  40280  cdleme43bN  40447  cdleme43dN  40449  cdlemeg46nlpq  40474  cdlemg12  40607  dihmeetcN  41259  dihjatc1  41268  dihjatcclem1  41375  lclkrlem2a  41464  lcfrlem20  41519  mapdh6aN  41692  mapdh8ab  41734  hdmap1l6a  41766  aks4d1p8d1  42041  fimgmcyc  42489  dffltz  42589  flt4lem5a  42607  flt4lem5b  42608  flt4lem5c  42609  flt4lem5d  42610  flt4lem5e  42611  irrapxlem1  42778  elpell14qr2  42818  elpell1qr2  42828  wepwsolem  42999  fnwe2lem2  43008  brneqtrd  44978  oddfl  45192  dstregt0  45196  xrlttri5d  45198  divlt0gt0d  45201  supxrgere  45248  supxrgelem  45252  supxrge  45253  suplesup  45254  nepnfltpnf  45257  nemnftgtmnft  45259  infrpge  45266  absimnre  45392  iccdifprioo  45434  climfveq  45590  climfveqf  45601  stoweidlem34  45955  stirlinglem5  45999  dirker2re  46013  dirkerdenne0  46014  dirkertrigeq  46022  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem54  46081  elaa2lem  46154  etransclem9  46164  sge0cl  46302  sge0repnf  46307  sge0split  46330  sge0gtfsumgt  46364  tworepnotupword  46805  lighneallem1  47479  lighneallem3  47481  0nodd  47893  2nodd  47895  1neven  47961