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  2851  eueq3  3685  efrirr  5621  efrn2lp  5622  epne3  7752  dif1enlem  9126  dif1enlemOLD  9127  ordtypelem9  9486  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1  9649  cnfcom3lem  9663  cflim2  10223  fin23lem30  10302  isf32lem5  10317  axdc3lem4  10413  axpownd  10561  pwfseqlem3  10620  grur1  10780  genpnnp  10965  xrlttri  13106  expneg  14041  bcval5  14290  seqcoll  14436  seqcoll2  14437  hashge2el2dif  14452  fsumss  15698  fprodss  15921  oddsumodd  16367  rpdvds  16637  pcmpt  16870  prmreclem2  16895  prmreclem5  16898  prmlem0  17083  sylow1lem3  19537  sylow2blem3  19559  efgredlema  19677  gsum2d2lem  19910  simpgnideld  20038  lindsind2  21735  1stccnp  23356  kqdisj  23626  alexsubALTlem4  23944  xrhmeo  24851  minveclem3b  25335  ovolgelb  25388  volsup  25464  volsup2  25513  itg1val2  25592  itg2seq  25650  itg2cn  25671  limcnlp  25786  itgsubstlem  25962  ply1termlem  26115  radcnvlt1  26334  fsumharmonic  26929  ftalem3  26992  chpub  27138  lgsqr  27269  lgseisenlem1  27293  lgsquadlem3  27300  2sqlem8a  27343  2sqlem8  27344  2sqblem  27349  nosupbnd1lem2  27628  nosupbnd2  27635  noinfbnd1lem2  27643  noinfbnd2  27650  axtgupdim2  28405  tgdim01  28441  lnoppnhpg  28698  axcontlem2  28899  minvecolem5  30817  divnumden2  32747  qsnzr  33433  mxidlirred  33450  rprmndvdsr1  33502  resssra  33590  esum2d  34090  oddpwdc  34352  eulerpartlemsv2  34356  eulerpartlemv  34362  eulerpartlemgh  34376  signslema  34560  erdszelem7  35191  erdszelem8  35192  wsuclem  35820  knoppndvlem10  36516  knoppndvlem13  36519  nlpineqsn  37403  lindsdom  37615  ftc1anclem5  37698  cntotbnd  37797  lshpdisj  38987  lcv1  39041  atlatmstc  39319  hlatcon2  39453  4noncolr3  39454  3atlem6  39489  lplnnleat  39543  lplnexllnN  39565  lvolnleat  39584  4atlem11  39610  dalem1  39660  dalemswapyzps  39691  dalemrotps  39692  2llnma1  39788  dalawlem15  39886  4atexlemcnd  40073  ltrnel  40140  cdleme15c  40277  cdleme0nex  40291  cdleme20m  40324  cdleme43bN  40491  cdleme43dN  40493  cdlemeg46nlpq  40518  cdlemg12  40651  dihmeetcN  41303  dihjatc1  41312  dihjatcclem1  41419  lclkrlem2a  41508  lcfrlem20  41563  mapdh6aN  41736  mapdh8ab  41778  hdmap1l6a  41810  aks4d1p8d1  42079  mulltgt0d  42477  mullt0b2d  42479  sn-mullt0d  42480  fimgmcyc  42529  dffltz  42629  flt4lem5a  42647  flt4lem5b  42648  flt4lem5c  42649  flt4lem5d  42650  flt4lem5e  42651  irrapxlem1  42817  elpell14qr2  42857  elpell1qr2  42867  wepwsolem  43038  fnwe2lem2  43047  brneqtrd  45077  oddfl  45283  dstregt0  45287  xrlttri5d  45289  divlt0gt0d  45291  supxrgere  45336  supxrgelem  45340  supxrge  45341  suplesup  45342  nepnfltpnf  45345  nemnftgtmnft  45347  infrpge  45354  absimnre  45479  iccdifprioo  45521  climfveq  45674  climfveqf  45685  stoweidlem34  46039  stirlinglem5  46083  dirker2re  46097  dirkerdenne0  46098  dirkertrigeq  46106  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem54  46165  elaa2lem  46238  etransclem9  46248  sge0cl  46386  sge0repnf  46391  sge0split  46414  sge0gtfsumgt  46448  tworepnotupword  46891  mod2addne  47369  lighneallem1  47610  lighneallem3  47612  gpg3kgrtriexlem5  48082  0nodd  48162  2nodd  48164  1neven  48230