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  2857  eueq3  3668  efrirr  5603  efrn2lp  5604  epne3  7718  dif1enlem  9086  ordtypelem9  9433  cantnfp1lem3  9591  cantnflem1b  9597  cantnflem1  9600  cnfcom3lem  9614  cflim2  10175  fin23lem30  10254  isf32lem5  10269  axdc3lem4  10365  axpownd  10514  pwfseqlem3  10573  grur1  10733  genpnnp  10918  xrlttri  13055  expneg  13994  bcval5  14243  seqcoll  14389  seqcoll2  14390  hashge2el2dif  14405  fsumss  15650  fprodss  15873  oddsumodd  16319  rpdvds  16589  pcmpt  16822  prmreclem2  16847  prmreclem5  16850  prmlem0  17035  sylow1lem3  19531  sylow2blem3  19553  efgredlema  19671  gsum2d2lem  19904  simpgnideld  20032  lindsind2  21776  1stccnp  23408  kqdisj  23678  alexsubALTlem4  23996  xrhmeo  24902  minveclem3b  25386  ovolgelb  25439  volsup  25515  volsup2  25564  itg1val2  25643  itg2seq  25701  itg2cn  25722  limcnlp  25837  itgsubstlem  26013  ply1termlem  26166  radcnvlt1  26385  fsumharmonic  26980  ftalem3  27043  chpub  27189  lgsqr  27320  lgseisenlem1  27344  lgsquadlem3  27351  2sqlem8a  27394  2sqlem8  27395  2sqblem  27400  nosupbnd1lem2  27679  nosupbnd2  27686  noinfbnd1lem2  27694  noinfbnd2  27701  axtgupdim2  28524  tgdim01  28560  lnoppnhpg  28817  axcontlem2  29019  minvecolem5  30937  divnumden2  32875  qsnzr  33515  mxidlirred  33532  rprmndvdsr1  33584  esplyind  33710  resssra  33722  extdgfialglem1  33828  esum2d  34229  oddpwdc  34490  eulerpartlemsv2  34494  eulerpartlemv  34500  eulerpartlemgh  34514  signslema  34698  erdszelem7  35370  erdszelem8  35371  wsuclem  35996  knoppndvlem10  36694  knoppndvlem13  36697  nlpineqsn  37582  lindsdom  37784  ftc1anclem5  37867  cntotbnd  37966  lshpdisj  39282  lcv1  39336  atlatmstc  39614  hlatcon2  39747  4noncolr3  39748  3atlem6  39783  lplnnleat  39837  lplnexllnN  39859  lvolnleat  39878  4atlem11  39904  dalem1  39954  dalemswapyzps  39985  dalemrotps  39986  2llnma1  40082  dalawlem15  40180  4atexlemcnd  40367  ltrnel  40434  cdleme15c  40571  cdleme0nex  40585  cdleme20m  40618  cdleme43bN  40785  cdleme43dN  40787  cdlemeg46nlpq  40812  cdlemg12  40945  dihmeetcN  41597  dihjatc1  41606  dihjatcclem1  41713  lclkrlem2a  41802  lcfrlem20  41857  mapdh6aN  42030  mapdh8ab  42072  hdmap1l6a  42104  aks4d1p8d1  42373  mulltgt0d  42774  mullt0b2d  42776  sn-mullt0d  42777  fimgmcyc  42826  dffltz  42914  flt4lem5a  42932  flt4lem5b  42933  flt4lem5c  42934  flt4lem5d  42935  flt4lem5e  42936  irrapxlem1  43101  elpell14qr2  43141  elpell1qr2  43151  wepwsolem  43321  fnwe2lem2  43330  brneqtrd  45358  oddfl  45563  dstregt0  45567  xrlttri5d  45569  divlt0gt0d  45571  supxrgere  45615  supxrgelem  45619  supxrge  45620  suplesup  45621  nepnfltpnf  45624  nemnftgtmnft  45626  infrpge  45633  absimnre  45757  iccdifprioo  45799  climfveq  45950  climfveqf  45961  stoweidlem34  46315  stirlinglem5  46359  dirker2re  46373  dirkerdenne0  46374  dirkertrigeq  46382  dirkercncflem2  46385  dirkercncflem4  46387  fourierdlem54  46441  elaa2lem  46514  etransclem9  46524  sge0cl  46662  sge0repnf  46667  sge0split  46690  sge0gtfsumgt  46724  mod2addne  47647  lighneallem1  47888  lighneallem3  47890  gpg3kgrtriexlem5  48370  0nodd  48453  2nodd  48455  1neven  48521