Theorem mtbid 327

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 251	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtod 201	1 ⊢ (𝜑 → ¬ 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  neleqtrd  2884  eueq3  3672  efrirr  5639  efrn2lp  5640  epne3  7775  dif1enlem  9157  ordtypelem9  9501  cantnfp1lem3  9662  cantnflem1b  9668  cantnflem1  9671  cnfcom3lem  9685  cflim2  10268  fin23lem30  10347  isf32lem5  10362  axdc3lem4  10458  axpownd  10613  pwfseqlem3  10672  grur1  10832  genpnnp  11017  xrlttri  13192  expneg  14135  bcval5  14384  seqcoll  14531  seqcoll2  14532  hashge2el2dif  14547  fsumss  15813  fprodss  16039  oddsumodd  16484  rpdvds  16754  pcmpt  16988  prmreclem2  17013  prmreclem5  17016  prmlem0  17201  sylow1lem3  19728  sylow2blem3  19750  efgredlema  19868  gsum2d2lem  20101  simpgnideld  20229  qsnzr  21547  lindsind2  22033  lindsdom  22064  1stccnp  23689  kqdisj  23959  alexsubALTlem4  24277  xrhmeo  25175  minveclem3b  25657  ovolgelb  25709  volsup  25785  volsup2  25834  itg1val2  25913  itg2seq  25971  itg2cn  25992  limcnlp  26107  itgsubstlem  26277  ply1termlem  26430  radcnvlt1  26651  fsumharmonic  27246  ftalem3  27309  chpub  27454  lgsqr  27585  lgseisenlem1  27609  lgsquadlem3  27616  2sqlem8a  27659  2sqlem8  27660  2sqblem  27665  nosupbnd1lem2  27943  nosupbnd2  27950  noinfbnd1lem2  27958  noinfbnd2  27965  axtgupdim2  28810  tgdim01  28847  lnoppnhpg  29119  axcontlem2  29408  minvecolem5  31348  divnumden2  33273  mxidlirred  33862  rprmndvdsr1  33921  esplyind  34072  resssra  34084  extdgfialglem1  34189  esum2d  34590  oddpwdc  34852  eulerpartlemsv2  34856  eulerpartlemv  34862  eulerpartlemgh  34876  signslema  35057  erdszelem7  35763  erdszelem8  35764  wsuclem  36389  knoppndvlem10  37205  knoppndvlem13  37208  nlpineqsn  38149  ftc1anclem5  38433  cntotbnd  38533  lshpdisj  39847  lcv1  39901  atlatmstc  40179  hlatcon2  40312  4noncolr3  40313  3atlem6  40348  lplnnleat  40402  lplnexllnN  40424  lvolnleat  40443  4atlem11  40469  dalem1  40519  dalemswapyzps  40550  dalemrotps  40551  2llnma1  40647  dalawlem15  40745  4atexlemcnd  40932  ltrnel  40999  cdleme15c  41136  cdleme0nex  41150  cdleme20m  41183  cdleme43bN  41350  cdleme43dN  41352  cdlemeg46nlpq  41377  cdlemg12  41510  dihmeetcN  42162  dihjatc1  42171  dihjatcclem1  42278  lclkrlem2a  42367  lcfrlem20  42422  mapdh6aN  42595  mapdh8ab  42637  hdmap1l6a  42669  aks4d1p8d1  42937  mulltgt0d  43357  mullt0b2d  43359  sn-mullt0d  43360  fimgmcyc  43403  dffltz  43467  flt4lem5a  43485  flt4lem5b  43486  flt4lem5c  43487  flt4lem5d  43488  flt4lem5e  43489  irrapxlem1  43650  elpell14qr2  43690  elpell1qr2  43700  wepwsolem  43870  fnwe2lem2  43879  brneqtrd  45897  oddfl  46098  dstregt0  46102  xrlttri5d  46104  divlt0gt0d  46106  supxrgere  46150  supxrgelem  46154  supxrge  46155  suplesup  46156  nepnfltpnf  46159  nemnftgtmnft  46161  infrpge  46168  absimnre  46291  iccdifprioo  46333  climfveq  46484  climfveqf  46495  stoweidlem34  46849  stirlinglem5  46893  dirker2re  46907  dirkerdenne0  46908  dirkertrigeq  46916  dirkercncflem2  46919  dirkercncflem4  46921  fourierdlem54  46975  elaa2lem  47048  etransclem9  47058  sge0cl  47196  sge0repnf  47201  sge0split  47224  sge0gtfsumgt  47258  mod2addne  48245  lighneallem1  48495  lighneallem3  48497  gpg3kgrtriexlem5  48990  0nodd  49072  2nodd  49074  1neven  49140  veroquaddetzerod  50806