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 ⊢ (𝜑 → ¬ 𝜒)

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

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 210

This theorem is referenced by:  neleqtrd  2911  eueq3  3650  efrirr  5500  efrn2lp  5501  epne3  7475  wfrlem10  7947  ordtypelem9  8974  cantnfp1lem3  9127  cantnflem1b  9133  cantnflem1  9136  cnfcom3lem  9150  cflim2  9674  fin23lem30  9753  isf32lem5  9768  axdc3lem4  9864  axpownd  10012  pwfseqlem3  10071  grur1  10231  genpnnp  10416  xrlttri  12520  expneg  13433  bcval5  13674  seqcoll  13818  seqcoll2  13819  hashge2el2dif  13834  fsumss  15074  fprodss  15294  oddsumodd  15731  rpdvds  15994  pcmpt  16218  prmreclem2  16243  prmreclem5  16246  prmlem0  16431  sylow1lem3  18717  sylow2blem3  18739  efgredlema  18858  gsum2d2lem  19086  simpgnideld  19214  lindsind2  20508  1stccnp  22067  kqdisj  22337  alexsubALTlem4  22655  xrhmeo  23551  minveclem3b  24032  ovolgelb  24084  volsup  24160  volsup2  24209  itg1val2  24288  itg2seq  24346  itg2cn  24367  limcnlp  24481  itgsubstlem  24651  ply1termlem  24800  radcnvlt1  25013  fsumharmonic  25597  ftalem3  25660  chpub  25804  lgsqr  25935  lgseisenlem1  25959  lgsquadlem3  25966  2sqlem8a  26009  2sqlem8  26010  2sqblem  26015  axtgupdim2  26265  tgdim01  26301  lnoppnhpg  26558  axcontlem2  26759  minvecolem5  28664  divnumden2  30560  esum2d  31462  oddpwdc  31722  eulerpartlemsv2  31726  eulerpartlemv  31732  eulerpartlemgh  31746  signslema  31942  erdszelem7  32557  erdszelem8  32558  wsuclem  33225  nosupbnd1lem2  33322  nosupbnd2  33329  knoppndvlem10  33973  knoppndvlem13  33976  nlpineqsn  34825  lindsdom  35051  ftc1anclem5  35134  cntotbnd  35234  lshpdisj  36283  lcv1  36337  atlatmstc  36615  hlatcon2  36748  4noncolr3  36749  3atlem6  36784  lplnnleat  36838  lplnexllnN  36860  lvolnleat  36879  4atlem11  36905  dalem1  36955  dalemswapyzps  36986  dalemrotps  36987  2llnma1  37083  dalawlem15  37181  4atexlemcnd  37368  ltrnel  37435  cdleme15c  37572  cdleme0nex  37586  cdleme20m  37619  cdleme43bN  37786  cdleme43dN  37788  cdlemeg46nlpq  37813  cdlemg12  37946  dihmeetcN  38598  dihjatc1  38607  dihjatcclem1  38714  lclkrlem2a  38803  lcfrlem20  38858  mapdh6aN  39031  mapdh8ab  39073  hdmap1l6a  39105  dffltz  39615  irrapxlem1  39763  elpell14qr2  39803  elpell1qr2  39813  wepwsolem  39986  fnwe2lem2  39995  brneqtrd  41712  oddfl  41908  dstregt0  41912  xrlttri5d  41914  divlt0gt0d  41917  supxrgere  41965  supxrgelem  41969  supxrge  41970  suplesup  41971  nepnfltpnf  41974  nemnftgtmnft  41976  infrpge  41983  absimnre  42116  iccdifprioo  42153  climfveq  42311  climfveqf  42322  stoweidlem34  42676  stirlinglem5  42720  dirker2re  42734  dirkerdenne0  42735  dirkertrigeq  42743  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem54  42802  elaa2lem  42875  etransclem9  42885  sge0cl  43020  sge0repnf  43025  sge0split  43048  sge0gtfsumgt  43082  lighneallem1  44123  lighneallem3  44125  0nodd  44430  2nodd  44432  1neven  44556