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  2882  eueq3  3668  efrirr  5630  efrn2lp  5631  epne3  7787  fnwe2lem3  8147  dif1enlem  9175  ordtypelem9  9520  cantnfp1lem3  9681  cantnflem1b  9687  cantnflem1  9690  cnfcom3lem  9704  cflim2  10341  fin23lem30  10420  isf32lem5  10435  axdc3lem4  10531  axpownd  10686  pwfseqlem3  10745  grur1  10905  genpnnp  11090  xrlttri  13268  expneg  14212  bcval5  14462  seqcoll  14609  seqcoll2  14610  hashge2el2dif  14625  fsumss  15891  fprodss  16115  oddsumodd  16560  rpdvds  16835  pcmpt  17070  prmreclem2  17095  prmreclem5  17098  prmlem0  17283  sylow1lem3  19814  sylow2blem3  19836  efgredlema  19954  gsum2d2lem  20187  simpgnideld  20315  qsnzr  21639  lindsind2  22125  lindsdom  22156  1stccnp  23781  kqdisj  24051  alexsubALTlem4  24369  xrhmeo  25267  minveclem3b  25749  ovolgelb  25801  volsup  25877  volsup2  25926  itg1val2  26005  itg2seq  26063  itg2cn  26084  limcnlp  26198  itgsubstlem  26368  ply1termlem  26521  radcnvlt1  26745  fsumharmonic  27339  ftalem3  27402  chpub  27547  lgsqr  27678  lgseisenlem1  27702  lgsquadlem3  27709  2sqlem8a  27752  2sqlem8  27753  2sqblem  27758  flt4lem5a  27982  flt4lem5b  27983  flt4lem5c  27984  flt4lem5d  27985  flt4lem5e  27986  nosupbnd1lem2  28066  nosupbnd2  28073  noinfbnd1lem2  28081  noinfbnd2  28088  axtgupdim2  28933  tgdim01  28970  lnoppnhpg  29242  axcontlem2  29543  minvecolem5  31483  divnumden2  33407  mxidlirred  33997  rprmndvdsr1  34056  esplyind  34207  resssra  34219  extdgfialglem1  34324  esum2d  34725  oddpwdc  34986  eulerpartlemsv2  34990  eulerpartlemv  34996  eulerpartlemgh  35010  signslema  35191  erdszelem7  35962  erdszelem8  35963  wsuclem  36587  knoppndvlem10  37387  knoppndvlem13  37390  nlpineqsn  38332  ftc1anclem5  38616  cntotbnd  38731  lshpdisj  40045  lcv1  40099  atlatmstc  40377  hlatcon2  40510  4noncolr3  40511  3atlem6  40546  lplnnleat  40600  lplnexllnN  40622  lvolnleat  40641  4atlem11  40667  dalem1  40717  dalemswapyzps  40748  dalemrotps  40749  2llnma1  40845  dalawlem15  40943  4atexlemcnd  41130  ltrnel  41197  cdleme15c  41334  cdleme0nex  41348  cdleme20m  41381  cdleme43bN  41548  cdleme43dN  41550  cdlemeg46nlpq  41575  cdlemg12  41708  dihmeetcN  42360  dihjatc1  42369  dihjatcclem1  42476  lclkrlem2a  42565  lcfrlem20  42620  mapdh6aN  42793  mapdh8ab  42835  hdmap1l6a  42867  aks4d1p8d1  43135  mulltgt0d  43547  mullt0b2d  43549  sn-mullt0d  43550  fimgmcyc  43599  dffltz  43671  irrapxlem1  43829  elpell14qr2  43869  elpell1qr2  43879  wepwsolem  44049  brneqtrd  46093  oddfl  46294  dstregt0  46298  xrlttri5d  46300  divlt0gt0d  46302  supxrgere  46345  supxrgelem  46349  supxrge  46350  suplesup  46351  nepnfltpnf  46354  nemnftgtmnft  46356  infrpge  46363  absimnre  46486  iccdifprioo  46528  climfveq  46679  climfveqf  46690  stoweidlem34  47044  stirlinglem5  47088  dirker2re  47102  dirkerdenne0  47103  dirkertrigeq  47111  dirkercncflem2  47114  dirkercncflem4  47116  fourierdlem54  47170  elaa2lem  47243  etransclem9  47253  sge0cl  47391  sge0repnf  47396  sge0split  47419  sge0gtfsumgt  47453  mod2addne  48440  lighneallem1  48690  lighneallem3  48692  gpg3kgrtriexlem5  49185  0nodd  49267  2nodd  49269  1neven  49335  veroquaddetzerod  50986