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  2882  eueq3  3668  efrirr  5630  efrn2lp  5631  epne3  7787  fnwe2lem3  8147  dif1enlem  9176  ordtypelem9  9521  cantnfp1lem3  9682  cantnflem1b  9688  cantnflem1  9691  cnfcom3lem  9705  cflim2  10342  fin23lem30  10421  isf32lem5  10436  axdc3lem4  10532  axpownd  10687  pwfseqlem3  10746  grur1  10906  genpnnp  11091  xrlttri  13269  expneg  14213  bcval5  14463  seqcoll  14610  seqcoll2  14611  hashge2el2dif  14626  fsumss  15892  fprodss  16116  oddsumodd  16561  rpdvds  16836  pcmpt  17071  prmreclem2  17096  prmreclem5  17099  prmlem0  17284  sylow1lem3  19815  sylow2blem3  19837  efgredlema  19955  gsum2d2lem  20188  simpgnideld  20316  qsnzr  21640  lindsind2  22126  lindsdom  22157  1stccnp  23782  kqdisj  24052  alexsubALTlem4  24370  xrhmeo  25268  minveclem3b  25750  ovolgelb  25802  volsup  25878  volsup2  25927  itg1val2  26006  itg2seq  26064  itg2cn  26085  limcnlp  26199  itgsubstlem  26369  ply1termlem  26522  radcnvlt1  26746  fsumharmonic  27340  ftalem3  27403  chpub  27548  lgsqr  27679  lgseisenlem1  27703  lgsquadlem3  27710  2sqlem8a  27753  2sqlem8  27754  2sqblem  27759  flt4lem5a  27983  flt4lem5b  27984  flt4lem5c  27985  flt4lem5d  27986  flt4lem5e  27987  nosupbnd1lem2  28067  nosupbnd2  28074  noinfbnd1lem2  28082  noinfbnd2  28089  axtgupdim2  28934  tgdim01  28971  lnoppnhpg  29243  axcontlem2  29544  minvecolem5  31484  tgextancd  33069  divnumden2  33450  mxidlirred  34040  rprmndvdsr1  34099  esplyind  34250  resssra  34262  extdgfialglem1  34367  esum2d  34768  oddpwdc  35029  eulerpartlemsv2  35033  eulerpartlemv  35039  eulerpartlemgh  35053  signslema  35234  erdszelem7  36031  erdszelem8  36032  wsuclem  36662  knoppndvlem10  37462  knoppndvlem13  37465  nlpineqsn  38407  ftc1anclem5  38691  cntotbnd  38806  lshpdisj  40120  lcv1  40174  atlatmstc  40452  hlatcon2  40585  4noncolr3  40586  3atlem6  40621  lplnnleat  40675  lplnexllnN  40697  lvolnleat  40716  4atlem11  40742  dalem1  40792  dalemswapyzps  40823  dalemrotps  40824  2llnma1  40920  dalawlem15  41018  4atexlemcnd  41205  ltrnel  41272  cdleme15c  41409  cdleme0nex  41423  cdleme20m  41456  cdleme43bN  41623  cdleme43dN  41625  cdlemeg46nlpq  41650  cdlemg12  41783  dihmeetcN  42435  dihjatc1  42444  dihjatcclem1  42551  lclkrlem2a  42640  lcfrlem20  42695  mapdh6aN  42868  mapdh8ab  42910  hdmap1l6a  42942  aks4d1p8d1  43210  mulltgt0d  43622  mullt0b2d  43624  sn-mullt0d  43625  fimgmcyc  43674  dffltz  43746  irrapxlem1  43905  elpell14qr2  43945  elpell1qr2  43955  wepwsolem  44125  brneqtrd  46169  oddfl  46370  dstregt0  46374  xrlttri5d  46376  divlt0gt0d  46378  supxrgere  46421  supxrgelem  46425  supxrge  46426  suplesup  46427  nepnfltpnf  46430  nemnftgtmnft  46432  infrpge  46439  absimnre  46562  iccdifprioo  46604  climfveq  46755  climfveqf  46766  stoweidlem34  47120  stirlinglem5  47164  dirker2re  47178  dirkerdenne0  47179  dirkertrigeq  47187  dirkercncflem2  47190  dirkercncflem4  47192  fourierdlem54  47246  elaa2lem  47319  etransclem9  47329  sge0cl  47467  sge0repnf  47472  sge0split  47495  sge0gtfsumgt  47529  mod2addne  48516  lighneallem1  48766  lighneallem3  48768  gpg3kgrtriexlem5  49261  0nodd  49343  2nodd  49345  1neven  49411  veroquaddetzerod  51062