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  2886  eueq3  3672  efrirr  5635  efrn2lp  5636  epne3  7808  fnwe2lem3  8171  dif1enlem  9200  ordtypelem9  9544  cantnfp1lem3  9705  cantnflem1b  9711  cantnflem1  9714  cnfcom3lem  9728  cflim2  10365  fin23lem30  10444  isf32lem5  10459  axdc3lem4  10555  axpownd  10710  pwfseqlem3  10769  grur1  10929  genpnnp  11114  xrlttri  13292  expneg  14236  bcval5  14486  seqcoll  14633  seqcoll2  14634  hashge2el2dif  14649  fsumss  15917  fprodss  16141  oddsumodd  16586  rpdvds  16861  pcmpt  17096  prmreclem2  17121  prmreclem5  17124  prmlem0  17309  sylow1lem3  19841  sylow2blem3  19863  efgredlema  19981  gsum2d2lem  20214  simpgnideld  20342  qsnzr  21666  lindsind2  22152  lindsdom  22183  1stccnp  23808  kqdisj  24078  alexsubALTlem4  24396  xrhmeo  25294  minveclem3b  25776  ovolgelb  25828  volsup  25904  volsup2  25953  itg1val2  26032  itg2seq  26090  itg2cn  26111  limcnlp  26225  itgsubstlem  26395  ply1termlem  26548  radcnvlt1  26772  fsumharmonic  27366  ftalem3  27429  chpub  27574  lgsqr  27705  lgseisenlem1  27729  lgsquadlem3  27736  2sqlem8a  27779  2sqlem8  27780  2sqblem  27785  flt4lem5a  28009  flt4lem5b  28010  flt4lem5c  28011  flt4lem5d  28012  flt4lem5e  28013  nosupbnd1lem2  28093  nosupbnd2  28100  noinfbnd1lem2  28108  noinfbnd2  28115  axtgupdim2  28960  tgdim01  28997  lnoppnhpg  29269  axcontlem2  29570  minvecolem5  31510  tgextancd  33095  divnumden2  33474  mxidlirred  34064  rprmndvdsr1  34123  esplyind  34274  resssra  34286  extdgfialglem1  34391  esum2d  34792  oddpwdc  35053  eulerpartlemsv2  35057  eulerpartlemv  35063  eulerpartlemgh  35077  signslema  35258  erdszelem7  36128  erdszelem8  36129  wsuclem  36764  knoppndvlem10  37564  knoppndvlem13  37567  nlpineqsn  38522  ftc1anclem5  38806  cntotbnd  38921  lshpdisj  40235  lcv1  40289  atlatmstc  40567  hlatcon2  40700  4noncolr3  40701  3atlem6  40736  lplnnleat  40790  lplnexllnN  40812  lvolnleat  40831  4atlem11  40857  dalem1  40907  dalemswapyzps  40938  dalemrotps  40939  2llnma1  41035  dalawlem15  41133  4atexlemcnd  41320  ltrnel  41387  cdleme15c  41524  cdleme0nex  41538  cdleme20m  41571  cdleme43bN  41738  cdleme43dN  41740  cdlemeg46nlpq  41765  cdlemg12  41898  dihmeetcN  42550  dihjatc1  42559  dihjatcclem1  42666  lclkrlem2a  42755  lcfrlem20  42810  mapdh6aN  42983  mapdh8ab  43025  hdmap1l6a  43057  aks4d1p8d1  43325  mulltgt0d  43737  mullt0b2d  43739  sn-mullt0d  43740  fimgmcyc  43789  dffltz  43861  irrapxlem1  44020  elpell14qr2  44060  elpell1qr2  44070  wepwsolem  44240  brneqtrd  46296  oddfl  46497  dstregt0  46501  xrlttri5d  46503  divlt0gt0d  46505  supxrgere  46548  supxrgelem  46552  supxrge  46553  suplesup  46554  nepnfltpnf  46557  nemnftgtmnft  46559  infrpge  46566  absimnre  46689  iccdifprioo  46731  climfveq  46882  climfveqf  46893  stoweidlem34  47247  stirlinglem5  47291  dirker2re  47305  dirkerdenne0  47306  dirkertrigeq  47314  dirkercncflem2  47317  dirkercncflem4  47319  fourierdlem54  47373  elaa2lem  47446  etransclem9  47456  sge0cl  47594  sge0repnf  47599  sge0split  47622  sge0gtfsumgt  47656  mod2addne  48643  lighneallem1  48893  lighneallem3  48895  gpg3kgrtriexlem5  49388  0nodd  49470  2nodd  49472  1neven  49538  veroquaddetzerod  51264