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  3671  efrirr  5599  efrn2lp  5600  epne3  7709  dif1enlem  9073  ordtypelem9  9418  cantnfp1lem3  9576  cantnflem1b  9582  cantnflem1  9585  cnfcom3lem  9599  cflim2  10157  fin23lem30  10236  isf32lem5  10251  axdc3lem4  10347  axpownd  10495  pwfseqlem3  10554  grur1  10714  genpnnp  10899  xrlttri  13041  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  19479  sylow2blem3  19501  efgredlema  19619  gsum2d2lem  19852  simpgnideld  19980  lindsind2  21726  1stccnp  23347  kqdisj  23617  alexsubALTlem4  23935  xrhmeo  24842  minveclem3b  25326  ovolgelb  25379  volsup  25455  volsup2  25504  itg1val2  25583  itg2seq  25641  itg2cn  25662  limcnlp  25777  itgsubstlem  25953  ply1termlem  26106  radcnvlt1  26325  fsumharmonic  26920  ftalem3  26983  chpub  27129  lgsqr  27260  lgseisenlem1  27284  lgsquadlem3  27291  2sqlem8a  27334  2sqlem8  27335  2sqblem  27340  nosupbnd1lem2  27619  nosupbnd2  27626  noinfbnd1lem2  27634  noinfbnd2  27641  axtgupdim2  28420  tgdim01  28456  lnoppnhpg  28713  axcontlem2  28914  minvecolem5  30829  divnumden2  32769  qsnzr  33401  mxidlirred  33418  rprmndvdsr1  33470  resssra  33569  extdgfialglem1  33675  esum2d  34076  oddpwdc  34338  eulerpartlemsv2  34342  eulerpartlemv  34348  eulerpartlemgh  34362  signslema  34546  erdszelem7  35190  erdszelem8  35191  wsuclem  35819  knoppndvlem10  36515  knoppndvlem13  36518  nlpineqsn  37402  lindsdom  37614  ftc1anclem5  37697  cntotbnd  37796  lshpdisj  38986  lcv1  39040  atlatmstc  39318  hlatcon2  39451  4noncolr3  39452  3atlem6  39487  lplnnleat  39541  lplnexllnN  39563  lvolnleat  39582  4atlem11  39608  dalem1  39658  dalemswapyzps  39689  dalemrotps  39690  2llnma1  39786  dalawlem15  39884  4atexlemcnd  40071  ltrnel  40138  cdleme15c  40275  cdleme0nex  40289  cdleme20m  40322  cdleme43bN  40489  cdleme43dN  40491  cdlemeg46nlpq  40516  cdlemg12  40649  dihmeetcN  41301  dihjatc1  41310  dihjatcclem1  41417  lclkrlem2a  41506  lcfrlem20  41561  mapdh6aN  41734  mapdh8ab  41776  hdmap1l6a  41808  aks4d1p8d1  42077  mulltgt0d  42475  mullt0b2d  42477  sn-mullt0d  42478  fimgmcyc  42527  dffltz  42627  flt4lem5a  42645  flt4lem5b  42646  flt4lem5c  42647  flt4lem5d  42648  flt4lem5e  42649  irrapxlem1  42815  elpell14qr2  42855  elpell1qr2  42865  wepwsolem  43035  fnwe2lem2  43044  brneqtrd  45074  oddfl  45280  dstregt0  45284  xrlttri5d  45286  divlt0gt0d  45288  supxrgere  45333  supxrgelem  45337  supxrge  45338  suplesup  45339  nepnfltpnf  45342  nemnftgtmnft  45344  infrpge  45351  absimnre  45475  iccdifprioo  45517  climfveq  45670  climfveqf  45681  stoweidlem34  46035  stirlinglem5  46079  dirker2re  46093  dirkerdenne0  46094  dirkertrigeq  46102  dirkercncflem2  46105  dirkercncflem4  46107  fourierdlem54  46161  elaa2lem  46234  etransclem9  46244  sge0cl  46382  sge0repnf  46387  sge0split  46410  sge0gtfsumgt  46444  tworepnotupword  46887  mod2addne  47368  lighneallem1  47609  lighneallem3  47611  gpg3kgrtriexlem5  48091  0nodd  48174  2nodd  48176  1neven  48242