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  2863  eueq3  3717  efrirr  5665  efrn2lp  5666  epne3  7793  wfrlem10OLD  8358  dif1enlem  9196  dif1enlemOLD  9197  ordtypelem9  9566  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1  9729  cnfcom3lem  9743  cflim2  10303  fin23lem30  10382  isf32lem5  10397  axdc3lem4  10493  axpownd  10641  pwfseqlem3  10700  grur1  10860  genpnnp  11045  xrlttri  13181  expneg  14110  bcval5  14357  seqcoll  14503  seqcoll2  14504  hashge2el2dif  14519  fsumss  15761  fprodss  15984  oddsumodd  16427  rpdvds  16697  pcmpt  16930  prmreclem2  16955  prmreclem5  16958  prmlem0  17143  sylow1lem3  19618  sylow2blem3  19640  efgredlema  19758  gsum2d2lem  19991  simpgnideld  20119  lindsind2  21839  1stccnp  23470  kqdisj  23740  alexsubALTlem4  24058  xrhmeo  24977  minveclem3b  25462  ovolgelb  25515  volsup  25591  volsup2  25640  itg1val2  25719  itg2seq  25777  itg2cn  25798  limcnlp  25913  itgsubstlem  26089  ply1termlem  26242  radcnvlt1  26461  fsumharmonic  27055  ftalem3  27118  chpub  27264  lgsqr  27395  lgseisenlem1  27419  lgsquadlem3  27426  2sqlem8a  27469  2sqlem8  27470  2sqblem  27475  nosupbnd1lem2  27754  nosupbnd2  27761  noinfbnd1lem2  27769  noinfbnd2  27776  axtgupdim2  28479  tgdim01  28515  lnoppnhpg  28772  axcontlem2  28980  minvecolem5  30900  divnumden2  32817  qsnzr  33483  mxidlirred  33500  rprmndvdsr1  33552  resssra  33638  esum2d  34094  oddpwdc  34356  eulerpartlemsv2  34360  eulerpartlemv  34366  eulerpartlemgh  34380  signslema  34577  erdszelem7  35202  erdszelem8  35203  wsuclem  35826  knoppndvlem10  36522  knoppndvlem13  36525  nlpineqsn  37409  lindsdom  37621  ftc1anclem5  37704  cntotbnd  37803  lshpdisj  38988  lcv1  39042  atlatmstc  39320  hlatcon2  39454  4noncolr3  39455  3atlem6  39490  lplnnleat  39544  lplnexllnN  39566  lvolnleat  39585  4atlem11  39611  dalem1  39661  dalemswapyzps  39692  dalemrotps  39693  2llnma1  39789  dalawlem15  39887  4atexlemcnd  40074  ltrnel  40141  cdleme15c  40278  cdleme0nex  40292  cdleme20m  40325  cdleme43bN  40492  cdleme43dN  40494  cdlemeg46nlpq  40519  cdlemg12  40652  dihmeetcN  41304  dihjatc1  41313  dihjatcclem1  41420  lclkrlem2a  41509  lcfrlem20  41564  mapdh6aN  41737  mapdh8ab  41779  hdmap1l6a  41811  aks4d1p8d1  42085  fimgmcyc  42544  dffltz  42644  flt4lem5a  42662  flt4lem5b  42663  flt4lem5c  42664  flt4lem5d  42665  flt4lem5e  42666  irrapxlem1  42833  elpell14qr2  42873  elpell1qr2  42883  wepwsolem  43054  fnwe2lem2  43063  brneqtrd  45081  oddfl  45289  dstregt0  45293  xrlttri5d  45295  divlt0gt0d  45298  supxrgere  45344  supxrgelem  45348  supxrge  45349  suplesup  45350  nepnfltpnf  45353  nemnftgtmnft  45355  infrpge  45362  absimnre  45487  iccdifprioo  45529  climfveq  45684  climfveqf  45695  stoweidlem34  46049  stirlinglem5  46093  dirker2re  46107  dirkerdenne0  46108  dirkertrigeq  46116  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem54  46175  elaa2lem  46248  etransclem9  46258  sge0cl  46396  sge0repnf  46401  sge0split  46424  sge0gtfsumgt  46458  tworepnotupword  46901  lighneallem1  47592  lighneallem3  47594  gpg3kgrtriexlem5  48043  0nodd  48086  2nodd  48088  1neven  48154