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  3679  efrirr  5611  efrn2lp  5612  epne3  7729  dif1enlem  9097  dif1enlemOLD  9098  ordtypelem9  9455  cantnfp1lem3  9611  cantnflem1b  9617  cantnflem1  9620  cnfcom3lem  9634  cflim2  10194  fin23lem30  10273  isf32lem5  10288  axdc3lem4  10384  axpownd  10532  pwfseqlem3  10591  grur1  10751  genpnnp  10936  xrlttri  13077  expneg  14012  bcval5  14261  seqcoll  14407  seqcoll2  14408  hashge2el2dif  14423  fsumss  15668  fprodss  15891  oddsumodd  16337  rpdvds  16607  pcmpt  16840  prmreclem2  16865  prmreclem5  16868  prmlem0  17053  sylow1lem3  19515  sylow2blem3  19537  efgredlema  19655  gsum2d2lem  19888  simpgnideld  20016  lindsind2  21762  1stccnp  23383  kqdisj  23653  alexsubALTlem4  23971  xrhmeo  24878  minveclem3b  25362  ovolgelb  25415  volsup  25491  volsup2  25540  itg1val2  25619  itg2seq  25677  itg2cn  25698  limcnlp  25813  itgsubstlem  25989  ply1termlem  26142  radcnvlt1  26361  fsumharmonic  26956  ftalem3  27019  chpub  27165  lgsqr  27296  lgseisenlem1  27320  lgsquadlem3  27327  2sqlem8a  27370  2sqlem8  27371  2sqblem  27376  nosupbnd1lem2  27655  nosupbnd2  27662  noinfbnd1lem2  27670  noinfbnd2  27677  axtgupdim2  28452  tgdim01  28488  lnoppnhpg  28745  axcontlem2  28946  minvecolem5  30861  divnumden2  32791  qsnzr  33420  mxidlirred  33437  rprmndvdsr1  33489  resssra  33577  esum2d  34077  oddpwdc  34339  eulerpartlemsv2  34343  eulerpartlemv  34349  eulerpartlemgh  34363  signslema  34547  erdszelem7  35178  erdszelem8  35179  wsuclem  35807  knoppndvlem10  36503  knoppndvlem13  36506  nlpineqsn  37390  lindsdom  37602  ftc1anclem5  37685  cntotbnd  37784  lshpdisj  38974  lcv1  39028  atlatmstc  39306  hlatcon2  39440  4noncolr3  39441  3atlem6  39476  lplnnleat  39530  lplnexllnN  39552  lvolnleat  39571  4atlem11  39597  dalem1  39647  dalemswapyzps  39678  dalemrotps  39679  2llnma1  39775  dalawlem15  39873  4atexlemcnd  40060  ltrnel  40127  cdleme15c  40264  cdleme0nex  40278  cdleme20m  40311  cdleme43bN  40478  cdleme43dN  40480  cdlemeg46nlpq  40505  cdlemg12  40638  dihmeetcN  41290  dihjatc1  41299  dihjatcclem1  41406  lclkrlem2a  41495  lcfrlem20  41550  mapdh6aN  41723  mapdh8ab  41765  hdmap1l6a  41797  aks4d1p8d1  42066  mulltgt0d  42464  mullt0b2d  42466  sn-mullt0d  42467  fimgmcyc  42516  dffltz  42616  flt4lem5a  42634  flt4lem5b  42635  flt4lem5c  42636  flt4lem5d  42637  flt4lem5e  42638  irrapxlem1  42804  elpell14qr2  42844  elpell1qr2  42854  wepwsolem  43025  fnwe2lem2  43034  brneqtrd  45064  oddfl  45270  dstregt0  45274  xrlttri5d  45276  divlt0gt0d  45278  supxrgere  45323  supxrgelem  45327  supxrge  45328  suplesup  45329  nepnfltpnf  45332  nemnftgtmnft  45334  infrpge  45341  absimnre  45466  iccdifprioo  45508  climfveq  45661  climfveqf  45672  stoweidlem34  46026  stirlinglem5  46070  dirker2re  46084  dirkerdenne0  46085  dirkertrigeq  46093  dirkercncflem2  46096  dirkercncflem4  46098  fourierdlem54  46152  elaa2lem  46225  etransclem9  46235  sge0cl  46373  sge0repnf  46378  sge0split  46401  sge0gtfsumgt  46435  tworepnotupword  46878  mod2addne  47359  lighneallem1  47600  lighneallem3  47602  gpg3kgrtriexlem5  48072  0nodd  48152  2nodd  48154  1neven  48220