Theorem mtbid 326

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  neleqtrd  2886  eueq3  3676  efrirr  5629  efrn2lp  5630  epne3  7758  dif1enlem  9130  ordtypelem9  9476  cantnfp1lem3  9637  cantnflem1b  9643  cantnflem1  9646  cnfcom3lem  9660  cflim2  10222  fin23lem30  10301  isf32lem5  10316  axdc3lem4  10412  axpownd  10561  pwfseqlem3  10620  grur1  10780  genpnnp  10965  xrlttri  13143  expneg  14084  bcval5  14333  seqcoll  14479  seqcoll2  14480  hashge2el2dif  14495  fsumss  15754  fprodss  15980  oddsumodd  16426  rpdvds  16696  pcmpt  16930  prmreclem2  16955  prmreclem5  16958  prmlem0  17143  sylow1lem3  19642  sylow2blem3  19664  efgredlema  19782  gsum2d2lem  20015  simpgnideld  20143  lindsind2  21873  1stccnp  23524  kqdisj  23794  alexsubALTlem4  24112  xrhmeo  25010  minveclem3b  25492  ovolgelb  25544  volsup  25620  volsup2  25669  itg1val2  25748  itg2seq  25806  itg2cn  25827  limcnlp  25942  itgsubstlem  26112  ply1termlem  26265  radcnvlt1  26483  fsumharmonic  27078  ftalem3  27141  chpub  27286  lgsqr  27417  lgseisenlem1  27441  lgsquadlem3  27448  2sqlem8a  27491  2sqlem8  27492  2sqblem  27497  nosupbnd1lem2  27775  nosupbnd2  27782  noinfbnd1lem2  27790  noinfbnd2  27797  axtgupdim2  28642  tgdim01  28678  lnoppnhpg  28939  axcontlem2  29168  minvecolem5  31086  divnumden2  33020  qsnzr  33644  mxidlirred  33662  rprmndvdsr1  33722  esplyind  33874  resssra  33886  extdgfialglem1  33991  esum2d  34392  oddpwdc  34653  eulerpartlemsv2  34657  eulerpartlemv  34663  eulerpartlemgh  34677  signslema  34858  erdszelem7  35552  erdszelem8  35553  wsuclem  36178  knoppndvlem10  36964  knoppndvlem13  36967  nlpineqsn  37907  lindsdom  38118  ftc1anclem5  38201  cntotbnd  38300  lshpdisj  39616  lcv1  39670  atlatmstc  39948  hlatcon2  40081  4noncolr3  40082  3atlem6  40117  lplnnleat  40171  lplnexllnN  40193  lvolnleat  40212  4atlem11  40238  dalem1  40288  dalemswapyzps  40319  dalemrotps  40320  2llnma1  40416  dalawlem15  40514  4atexlemcnd  40701  ltrnel  40768  cdleme15c  40905  cdleme0nex  40919  cdleme20m  40952  cdleme43bN  41119  cdleme43dN  41121  cdlemeg46nlpq  41146  cdlemg12  41279  dihmeetcN  41931  dihjatc1  41940  dihjatcclem1  42047  lclkrlem2a  42136  lcfrlem20  42191  mapdh6aN  42364  mapdh8ab  42406  hdmap1l6a  42438  aks4d1p8d1  42706  mulltgt0d  43109  mullt0b2d  43111  sn-mullt0d  43112  fimgmcyc  43157  dffltz  43221  flt4lem5a  43239  flt4lem5b  43240  flt4lem5c  43241  flt4lem5d  43242  flt4lem5e  43243  irrapxlem1  43404  elpell14qr2  43444  elpell1qr2  43454  wepwsolem  43624  fnwe2lem2  43633  brneqtrd  45661  oddfl  45862  dstregt0  45866  xrlttri5d  45868  divlt0gt0d  45870  supxrgere  45914  supxrgelem  45918  supxrge  45919  suplesup  45920  nepnfltpnf  45923  nemnftgtmnft  45925  infrpge  45932  absimnre  46055  iccdifprioo  46097  climfveq  46248  climfveqf  46259  stoweidlem34  46613  stirlinglem5  46657  dirker2re  46671  dirkerdenne0  46672  dirkertrigeq  46680  dirkercncflem2  46683  dirkercncflem4  46685  fourierdlem54  46739  elaa2lem  46812  etransclem9  46822  sge0cl  46960  sge0repnf  46965  sge0split  46988  sge0gtfsumgt  47022  mod2addne  47969  lighneallem1  48219  lighneallem3  48221  gpg3kgrtriexlem5  48714  0nodd  48797  2nodd  48799  1neven  48865