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  2884  eueq3  3673  efrirr  5640  efrn2lp  5641  epne3  7770  dif1enlem  9142  ordtypelem9  9486  cantnfp1lem3  9647  cantnflem1b  9653  cantnflem1  9656  cnfcom3lem  9670  cflim2  10253  fin23lem30  10332  isf32lem5  10347  axdc3lem4  10443  axpownd  10592  pwfseqlem3  10651  grur1  10811  genpnnp  10996  xrlttri  13170  expneg  14112  bcval5  14361  seqcoll  14508  seqcoll2  14509  hashge2el2dif  14524  fsumss  15783  fprodss  16009  oddsumodd  16454  rpdvds  16724  pcmpt  16958  prmreclem2  16983  prmreclem5  16986  prmlem0  17171  sylow1lem3  19676  sylow2blem3  19698  efgredlema  19816  gsum2d2lem  20049  simpgnideld  20177  qsnzr  21494  lindsind2  21980  1stccnp  23630  kqdisj  23900  alexsubALTlem4  24218  xrhmeo  25116  minveclem3b  25598  ovolgelb  25650  volsup  25726  volsup2  25775  itg1val2  25854  itg2seq  25912  itg2cn  25933  limcnlp  26048  itgsubstlem  26218  ply1termlem  26371  radcnvlt1  26592  fsumharmonic  27187  ftalem3  27250  chpub  27395  lgsqr  27526  lgseisenlem1  27550  lgsquadlem3  27557  2sqlem8a  27600  2sqlem8  27601  2sqblem  27606  nosupbnd1lem2  27884  nosupbnd2  27891  noinfbnd1lem2  27899  noinfbnd2  27906  axtgupdim2  28751  tgdim01  28787  lnoppnhpg  29057  axcontlem2  29326  minvecolem5  31244  divnumden2  33171  mxidlirred  33764  rprmndvdsr1  33823  esplyind  33974  resssra  33986  extdgfialglem1  34091  esum2d  34492  oddpwdc  34753  eulerpartlemsv2  34757  eulerpartlemv  34763  eulerpartlemgh  34777  signslema  34958  erdszelem7  35697  erdszelem8  35698  wsuclem  36323  knoppndvlem10  37138  knoppndvlem13  37141  nlpineqsn  38082  lindsdom  38293  ftc1anclem5  38376  cntotbnd  38475  lshpdisj  39789  lcv1  39843  atlatmstc  40121  hlatcon2  40254  4noncolr3  40255  3atlem6  40290  lplnnleat  40344  lplnexllnN  40366  lvolnleat  40385  4atlem11  40411  dalem1  40461  dalemswapyzps  40492  dalemrotps  40493  2llnma1  40589  dalawlem15  40687  4atexlemcnd  40874  ltrnel  40941  cdleme15c  41078  cdleme0nex  41092  cdleme20m  41125  cdleme43bN  41292  cdleme43dN  41294  cdlemeg46nlpq  41319  cdlemg12  41452  dihmeetcN  42104  dihjatc1  42113  dihjatcclem1  42220  lclkrlem2a  42309  lcfrlem20  42364  mapdh6aN  42537  mapdh8ab  42579  hdmap1l6a  42611  aks4d1p8d1  42879  mulltgt0d  43284  mullt0b2d  43286  sn-mullt0d  43287  fimgmcyc  43330  dffltz  43394  flt4lem5a  43412  flt4lem5b  43413  flt4lem5c  43414  flt4lem5d  43415  flt4lem5e  43416  irrapxlem1  43577  elpell14qr2  43617  elpell1qr2  43627  wepwsolem  43797  fnwe2lem2  43806  brneqtrd  45824  oddfl  46025  dstregt0  46029  xrlttri5d  46031  divlt0gt0d  46033  supxrgere  46077  supxrgelem  46081  supxrge  46082  suplesup  46083  nepnfltpnf  46086  nemnftgtmnft  46088  infrpge  46095  absimnre  46218  iccdifprioo  46260  climfveq  46411  climfveqf  46422  stoweidlem34  46776  stirlinglem5  46820  dirker2re  46834  dirkerdenne0  46835  dirkertrigeq  46843  dirkercncflem2  46846  dirkercncflem4  46848  fourierdlem54  46902  elaa2lem  46975  etransclem9  46985  sge0cl  47123  sge0repnf  47128  sge0split  47151  sge0gtfsumgt  47185  mod2addne  48135  lighneallem1  48385  lighneallem3  48387  gpg3kgrtriexlem5  48880  0nodd  48963  2nodd  48965  1neven  49031