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  39320  irrapxlem1  39468  elpell14qr2  39508  elpell1qr2  39518  wepwsolem  39691  fnwe2lem2  39700  brneqtrd  41389  oddfl  41592  dstregt0  41596  xrlttri5d  41598  divlt0gt0d  41601  supxrgere  41650  supxrgelem  41654  supxrge  41655  suplesup  41656  nepnfltpnf  41659  nemnftgtmnft  41661  infrpge  41668  absimnre  41802  iccdifprioo  41841  climfveq  41999  climfveqf  42010  stoweidlem34  42368  stirlinglem5  42412  dirker2re  42426  dirkerdenne0  42427  dirkertrigeq  42435  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem54  42494  elaa2lem  42567  etransclem9  42577  sge0cl  42712  sge0repnf  42717  sge0split  42740  sge0gtfsumgt  42774  lighneallem1  43819  lighneallem3  43821  0nodd  44126  2nodd  44128  1neven  44252