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

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

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 207

This theorem is referenced by:  neleqtrd  2856  eueq3  3694  efrirr  5634  efrn2lp  5635  epne3  7765  wfrlem10OLD  8330  dif1enlem  9168  dif1enlemOLD  9169  ordtypelem9  9538  cantnfp1lem3  9692  cantnflem1b  9698  cantnflem1  9701  cnfcom3lem  9715  cflim2  10275  fin23lem30  10354  isf32lem5  10369  axdc3lem4  10465  axpownd  10613  pwfseqlem3  10672  grur1  10832  genpnnp  11017  xrlttri  13153  expneg  14085  bcval5  14334  seqcoll  14480  seqcoll2  14481  hashge2el2dif  14496  fsumss  15739  fprodss  15962  oddsumodd  16407  rpdvds  16677  pcmpt  16910  prmreclem2  16935  prmreclem5  16938  prmlem0  17123  sylow1lem3  19579  sylow2blem3  19601  efgredlema  19719  gsum2d2lem  19952  simpgnideld  20080  lindsind2  21777  1stccnp  23398  kqdisj  23668  alexsubALTlem4  23986  xrhmeo  24893  minveclem3b  25378  ovolgelb  25431  volsup  25507  volsup2  25556  itg1val2  25635  itg2seq  25693  itg2cn  25714  limcnlp  25829  itgsubstlem  26005  ply1termlem  26158  radcnvlt1  26377  fsumharmonic  26972  ftalem3  27035  chpub  27181  lgsqr  27312  lgseisenlem1  27336  lgsquadlem3  27343  2sqlem8a  27386  2sqlem8  27387  2sqblem  27392  nosupbnd1lem2  27671  nosupbnd2  27678  noinfbnd1lem2  27686  noinfbnd2  27693  axtgupdim2  28396  tgdim01  28432  lnoppnhpg  28689  axcontlem2  28890  minvecolem5  30808  divnumden2  32740  qsnzr  33416  mxidlirred  33433  rprmndvdsr1  33485  resssra  33573  esum2d  34070  oddpwdc  34332  eulerpartlemsv2  34336  eulerpartlemv  34342  eulerpartlemgh  34356  signslema  34540  erdszelem7  35165  erdszelem8  35166  wsuclem  35789  knoppndvlem10  36485  knoppndvlem13  36488  nlpineqsn  37372  lindsdom  37584  ftc1anclem5  37667  cntotbnd  37766  lshpdisj  38951  lcv1  39005  atlatmstc  39283  hlatcon2  39417  4noncolr3  39418  3atlem6  39453  lplnnleat  39507  lplnexllnN  39529  lvolnleat  39548  4atlem11  39574  dalem1  39624  dalemswapyzps  39655  dalemrotps  39656  2llnma1  39752  dalawlem15  39850  4atexlemcnd  40037  ltrnel  40104  cdleme15c  40241  cdleme0nex  40255  cdleme20m  40288  cdleme43bN  40455  cdleme43dN  40457  cdlemeg46nlpq  40482  cdlemg12  40615  dihmeetcN  41267  dihjatc1  41276  dihjatcclem1  41383  lclkrlem2a  41472  lcfrlem20  41527  mapdh6aN  41700  mapdh8ab  41742  hdmap1l6a  41774  aks4d1p8d1  42043  fimgmcyc  42504  dffltz  42604  flt4lem5a  42622  flt4lem5b  42623  flt4lem5c  42624  flt4lem5d  42625  flt4lem5e  42626  irrapxlem1  42792  elpell14qr2  42832  elpell1qr2  42842  wepwsolem  43013  fnwe2lem2  43022  brneqtrd  45048  oddfl  45254  dstregt0  45258  xrlttri5d  45260  divlt0gt0d  45263  supxrgere  45308  supxrgelem  45312  supxrge  45313  suplesup  45314  nepnfltpnf  45317  nemnftgtmnft  45319  infrpge  45326  absimnre  45451  iccdifprioo  45493  climfveq  45646  climfveqf  45657  stoweidlem34  46011  stirlinglem5  46055  dirker2re  46069  dirkerdenne0  46070  dirkertrigeq  46078  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem54  46137  elaa2lem  46210  etransclem9  46220  sge0cl  46358  sge0repnf  46363  sge0split  46386  sge0gtfsumgt  46420  tworepnotupword  46863  lighneallem1  47567  lighneallem3  47569  gpg3kgrtriexlem5  48037  0nodd  48093  2nodd  48095  1neven  48161