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  2859  eueq3  3671  efrirr  5614  efrn2lp  5615  epne3  7730  dif1enlem  9098  ordtypelem9  9445  cantnfp1lem3  9603  cantnflem1b  9609  cantnflem1  9612  cnfcom3lem  9626  cflim2  10187  fin23lem30  10266  isf32lem5  10281  axdc3lem4  10377  axpownd  10526  pwfseqlem3  10585  grur1  10745  genpnnp  10930  xrlttri  13067  expneg  14006  bcval5  14255  seqcoll  14401  seqcoll2  14402  hashge2el2dif  14417  fsumss  15662  fprodss  15885  oddsumodd  16331  rpdvds  16601  pcmpt  16834  prmreclem2  16859  prmreclem5  16862  prmlem0  17047  sylow1lem3  19546  sylow2blem3  19568  efgredlema  19686  gsum2d2lem  19919  simpgnideld  20047  lindsind2  21791  1stccnp  23423  kqdisj  23693  alexsubALTlem4  24011  xrhmeo  24917  minveclem3b  25401  ovolgelb  25454  volsup  25530  volsup2  25579  itg1val2  25658  itg2seq  25716  itg2cn  25737  limcnlp  25852  itgsubstlem  26028  ply1termlem  26181  radcnvlt1  26400  fsumharmonic  26995  ftalem3  27058  chpub  27204  lgsqr  27335  lgseisenlem1  27359  lgsquadlem3  27366  2sqlem8a  27409  2sqlem8  27410  2sqblem  27415  nosupbnd1lem2  27694  nosupbnd2  27701  noinfbnd1lem2  27709  noinfbnd2  27716  axtgupdim2  28561  tgdim01  28597  lnoppnhpg  28854  axcontlem2  29056  minvecolem5  30975  divnumden2  32913  qsnzr  33554  mxidlirred  33571  rprmndvdsr1  33623  esplyind  33758  resssra  33770  extdgfialglem1  33876  esum2d  34277  oddpwdc  34538  eulerpartlemsv2  34542  eulerpartlemv  34548  eulerpartlemgh  34562  signslema  34746  erdszelem7  35419  erdszelem8  35420  wsuclem  36045  knoppndvlem10  36749  knoppndvlem13  36752  nlpineqsn  37690  lindsdom  37894  ftc1anclem5  37977  cntotbnd  38076  lshpdisj  39392  lcv1  39446  atlatmstc  39724  hlatcon2  39857  4noncolr3  39858  3atlem6  39893  lplnnleat  39947  lplnexllnN  39969  lvolnleat  39988  4atlem11  40014  dalem1  40064  dalemswapyzps  40095  dalemrotps  40096  2llnma1  40192  dalawlem15  40290  4atexlemcnd  40477  ltrnel  40544  cdleme15c  40681  cdleme0nex  40695  cdleme20m  40728  cdleme43bN  40895  cdleme43dN  40897  cdlemeg46nlpq  40922  cdlemg12  41055  dihmeetcN  41707  dihjatc1  41716  dihjatcclem1  41823  lclkrlem2a  41912  lcfrlem20  41967  mapdh6aN  42140  mapdh8ab  42182  hdmap1l6a  42214  aks4d1p8d1  42483  mulltgt0d  42881  mullt0b2d  42883  sn-mullt0d  42884  fimgmcyc  42933  dffltz  43021  flt4lem5a  43039  flt4lem5b  43040  flt4lem5c  43041  flt4lem5d  43042  flt4lem5e  43043  irrapxlem1  43208  elpell14qr2  43248  elpell1qr2  43258  wepwsolem  43428  fnwe2lem2  43437  brneqtrd  45465  oddfl  45669  dstregt0  45673  xrlttri5d  45675  divlt0gt0d  45677  supxrgere  45721  supxrgelem  45725  supxrge  45726  suplesup  45727  nepnfltpnf  45730  nemnftgtmnft  45732  infrpge  45739  absimnre  45863  iccdifprioo  45905  climfveq  46056  climfveqf  46067  stoweidlem34  46421  stirlinglem5  46465  dirker2re  46479  dirkerdenne0  46480  dirkertrigeq  46488  dirkercncflem2  46491  dirkercncflem4  46493  fourierdlem54  46547  elaa2lem  46620  etransclem9  46630  sge0cl  46768  sge0repnf  46773  sge0split  46796  sge0gtfsumgt  46830  mod2addne  47753  lighneallem1  47994  lighneallem3  47996  gpg3kgrtriexlem5  48476  0nodd  48559  2nodd  48561  1neven  48627