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  2934  eueq3  3702  efrirr  5536  efrn2lp  5537  epne3  7495  wfrlem10  7964  ordtypelem9  8990  cantnfp1lem3  9143  cantnflem1b  9149  cantnflem1  9152  cnfcom3lem  9166  cflim2  9685  fin23lem30  9764  isf32lem5  9779  axdc3lem4  9875  axpownd  10023  pwfseqlem3  10082  grur1  10242  genpnnp  10427  xrlttri  12533  expneg  13438  bcval5  13679  seqcoll  13823  seqcoll2  13824  hashge2el2dif  13839  fsumss  15082  fprodss  15302  oddsumodd  15741  rpdvds  16004  pcmpt  16228  prmreclem2  16253  prmreclem5  16256  prmlem0  16439  sylow1lem3  18725  sylow2blem3  18747  efgredlema  18866  gsum2d2lem  19093  simpgnideld  19221  lindsind2  20963  1stccnp  22070  kqdisj  22340  alexsubALTlem4  22658  xrhmeo  23550  minveclem3b  24031  ovolgelb  24081  volsup  24157  volsup2  24206  itg1val2  24285  itg2seq  24343  itg2cn  24364  limcnlp  24476  itgsubstlem  24645  ply1termlem  24793  radcnvlt1  25006  fsumharmonic  25589  ftalem3  25652  chpub  25796  lgsqr  25927  lgseisenlem1  25951  lgsquadlem3  25958  2sqlem8a  26001  2sqlem8  26002  2sqblem  26007  axtgupdim2  26257  tgdim01  26293  lnoppnhpg  26550  axcontlem2  26751  minvecolem5  28658  divnumden2  30534  esum2d  31352  oddpwdc  31612  eulerpartlemsv2  31616  eulerpartlemv  31622  eulerpartlemgh  31636  signslema  31832  erdszelem7  32444  erdszelem8  32445  wsuclem  33112  nosupbnd1lem2  33209  nosupbnd2  33216  knoppndvlem10  33860  knoppndvlem13  33863  nlpineqsn  34692  lindsdom  34901  ftc1anclem5  34986  cntotbnd  35089  lshpdisj  36138  lcv1  36192  atlatmstc  36470  hlatcon2  36603  4noncolr3  36604  3atlem6  36639  lplnnleat  36693  lplnexllnN  36715  lvolnleat  36734  4atlem11  36760  dalem1  36810  dalemswapyzps  36841  dalemrotps  36842  2llnma1  36938  dalawlem15  37036  4atexlemcnd  37223  ltrnel  37290  cdleme15c  37427  cdleme0nex  37441  cdleme20m  37474  cdleme43bN  37641  cdleme43dN  37643  cdlemeg46nlpq  37668  cdlemg12  37801  dihmeetcN  38453  dihjatc1  38462  dihjatcclem1  38569  lclkrlem2a  38658  lcfrlem20  38713  mapdh6aN  38886  mapdh8ab  38928  hdmap1l6a  38960  dffltz  39291  irrapxlem1  39439  elpell14qr2  39479  elpell1qr2  39489  wepwsolem  39662  fnwe2lem2  39671  brneqtrd  41360  oddfl  41563  dstregt0  41567  xrlttri5d  41569  divlt0gt0d  41572  supxrgere  41621  supxrgelem  41625  supxrge  41626  suplesup  41627  nepnfltpnf  41630  nemnftgtmnft  41632  infrpge  41639  absimnre  41773  iccdifprioo  41812  climfveq  41970  climfveqf  41981  stoweidlem34  42339  stirlinglem5  42383  dirker2re  42397  dirkerdenne0  42398  dirkertrigeq  42406  dirkercncflem2  42409  dirkercncflem4  42411  fourierdlem54  42465  elaa2lem  42538  etransclem9  42548  sge0cl  42683  sge0repnf  42688  sge0split  42711  sge0gtfsumgt  42745  lighneallem1  43790  lighneallem3  43792  0nodd  44097  2nodd  44099  1neven  44223