Theorem mtbid 324

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 247	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtod 197	1 ⊢ (𝜑 → ¬ 𝜒)

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

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 206

This theorem is referenced by:  neleqtrd  2861  eueq3  3647  efrirr  5571  efrn2lp  5572  epne3  7632  wfrlem10OLD  8158  dif1enlem  8952  ordtypelem9  9294  cantnfp1lem3  9447  cantnflem1b  9453  cantnflem1  9456  cnfcom3lem  9470  cflim2  10028  fin23lem30  10107  isf32lem5  10122  axdc3lem4  10218  axpownd  10366  pwfseqlem3  10425  grur1  10585  genpnnp  10770  xrlttri  12882  expneg  13799  bcval5  14041  seqcoll  14187  seqcoll2  14188  hashge2el2dif  14203  fsumss  15446  fprodss  15667  oddsumodd  16108  rpdvds  16374  pcmpt  16602  prmreclem2  16627  prmreclem5  16630  prmlem0  16816  sylow1lem3  19214  sylow2blem3  19236  efgredlema  19355  gsum2d2lem  19583  simpgnideld  19711  lindsind2  21035  1stccnp  22622  kqdisj  22892  alexsubALTlem4  23210  xrhmeo  24118  minveclem3b  24601  ovolgelb  24653  volsup  24729  volsup2  24778  itg1val2  24857  itg2seq  24916  itg2cn  24937  limcnlp  25051  itgsubstlem  25221  ply1termlem  25373  radcnvlt1  25586  fsumharmonic  26170  ftalem3  26233  chpub  26377  lgsqr  26508  lgseisenlem1  26532  lgsquadlem3  26539  2sqlem8a  26582  2sqlem8  26583  2sqblem  26588  axtgupdim2  26841  tgdim01  26877  lnoppnhpg  27134  axcontlem2  27342  minvecolem5  29252  divnumden2  31141  esum2d  32070  oddpwdc  32330  eulerpartlemsv2  32334  eulerpartlemv  32340  eulerpartlemgh  32354  signslema  32550  erdszelem7  33168  erdszelem8  33169  wsuclem  33828  nosupbnd1lem2  33921  nosupbnd2  33928  noinfbnd1lem2  33936  noinfbnd2  33943  knoppndvlem10  34710  knoppndvlem13  34713  nlpineqsn  35588  lindsdom  35780  ftc1anclem5  35863  cntotbnd  35963  lshpdisj  37008  lcv1  37062  atlatmstc  37340  hlatcon2  37473  4noncolr3  37474  3atlem6  37509  lplnnleat  37563  lplnexllnN  37585  lvolnleat  37604  4atlem11  37630  dalem1  37680  dalemswapyzps  37711  dalemrotps  37712  2llnma1  37808  dalawlem15  37906  4atexlemcnd  38093  ltrnel  38160  cdleme15c  38297  cdleme0nex  38311  cdleme20m  38344  cdleme43bN  38511  cdleme43dN  38513  cdlemeg46nlpq  38538  cdlemg12  38671  dihmeetcN  39323  dihjatc1  39332  dihjatcclem1  39439  lclkrlem2a  39528  lcfrlem20  39583  mapdh6aN  39756  mapdh8ab  39798  hdmap1l6a  39830  aks4d1p8d1  40099  dffltz  40478  flt4lem5a  40496  flt4lem5b  40497  flt4lem5c  40498  flt4lem5d  40499  flt4lem5e  40500  irrapxlem1  40651  elpell14qr2  40691  elpell1qr2  40701  wepwsolem  40874  fnwe2lem2  40883  brneqtrd  42633  oddfl  42823  dstregt0  42827  xrlttri5d  42829  divlt0gt0d  42832  supxrgere  42879  supxrgelem  42883  supxrge  42884  suplesup  42885  nepnfltpnf  42888  nemnftgtmnft  42890  infrpge  42897  absimnre  43024  iccdifprioo  43061  climfveq  43217  climfveqf  43228  stoweidlem34  43582  stirlinglem5  43626  dirker2re  43640  dirkerdenne0  43641  dirkertrigeq  43649  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem54  43708  elaa2lem  43781  etransclem9  43791  sge0cl  43926  sge0repnf  43931  sge0split  43954  sge0gtfsumgt  43988  lighneallem1  45068  lighneallem3  45070  0nodd  45375  2nodd  45377  1neven  45501  tworepnotupword  46532