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  2858  eueq3  3657  efrirr  5611  efrn2lp  5612  epne3  7727  dif1enlem  9094  ordtypelem9  9441  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1  9610  cnfcom3lem  9624  cflim2  10185  fin23lem30  10264  isf32lem5  10279  axdc3lem4  10375  axpownd  10524  pwfseqlem3  10583  grur1  10743  genpnnp  10928  xrlttri  13090  expneg  14031  bcval5  14280  seqcoll  14426  seqcoll2  14427  hashge2el2dif  14442  fsumss  15687  fprodss  15913  oddsumodd  16359  rpdvds  16629  pcmpt  16863  prmreclem2  16888  prmreclem5  16891  prmlem0  17076  sylow1lem3  19575  sylow2blem3  19597  efgredlema  19715  gsum2d2lem  19948  simpgnideld  20076  lindsind2  21799  1stccnp  23427  kqdisj  23697  alexsubALTlem4  24015  xrhmeo  24913  minveclem3b  25395  ovolgelb  25447  volsup  25523  volsup2  25572  itg1val2  25651  itg2seq  25709  itg2cn  25730  limcnlp  25845  itgsubstlem  26015  ply1termlem  26168  radcnvlt1  26383  fsumharmonic  26975  ftalem3  27038  chpub  27183  lgsqr  27314  lgseisenlem1  27338  lgsquadlem3  27345  2sqlem8a  27388  2sqlem8  27389  2sqblem  27394  nosupbnd1lem2  27673  nosupbnd2  27680  noinfbnd1lem2  27688  noinfbnd2  27695  axtgupdim2  28539  tgdim01  28575  lnoppnhpg  28832  axcontlem2  29034  minvecolem5  30952  divnumden2  32889  qsnzr  33515  mxidlirred  33532  rprmndvdsr1  33584  esplyind  33719  resssra  33731  extdgfialglem1  33836  esum2d  34237  oddpwdc  34498  eulerpartlemsv2  34502  eulerpartlemv  34508  eulerpartlemgh  34522  signslema  34706  erdszelem7  35379  erdszelem8  35380  wsuclem  36005  knoppndvlem10  36781  knoppndvlem13  36784  nlpineqsn  37724  lindsdom  37935  ftc1anclem5  38018  cntotbnd  38117  lshpdisj  39433  lcv1  39487  atlatmstc  39765  hlatcon2  39898  4noncolr3  39899  3atlem6  39934  lplnnleat  39988  lplnexllnN  40010  lvolnleat  40029  4atlem11  40055  dalem1  40105  dalemswapyzps  40136  dalemrotps  40137  2llnma1  40233  dalawlem15  40331  4atexlemcnd  40518  ltrnel  40585  cdleme15c  40722  cdleme0nex  40736  cdleme20m  40769  cdleme43bN  40936  cdleme43dN  40938  cdlemeg46nlpq  40963  cdlemg12  41096  dihmeetcN  41748  dihjatc1  41757  dihjatcclem1  41864  lclkrlem2a  41953  lcfrlem20  42008  mapdh6aN  42181  mapdh8ab  42223  hdmap1l6a  42255  aks4d1p8d1  42523  mulltgt0d  42927  mullt0b2d  42929  sn-mullt0d  42930  fimgmcyc  42979  dffltz  43067  flt4lem5a  43085  flt4lem5b  43086  flt4lem5c  43087  flt4lem5d  43088  flt4lem5e  43089  irrapxlem1  43250  elpell14qr2  43290  elpell1qr2  43300  wepwsolem  43470  fnwe2lem2  43479  brneqtrd  45507  oddfl  45711  dstregt0  45715  xrlttri5d  45717  divlt0gt0d  45719  supxrgere  45763  supxrgelem  45767  supxrge  45768  suplesup  45769  nepnfltpnf  45772  nemnftgtmnft  45774  infrpge  45781  absimnre  45904  iccdifprioo  45946  climfveq  46097  climfveqf  46108  stoweidlem34  46462  stirlinglem5  46506  dirker2re  46520  dirkerdenne0  46521  dirkertrigeq  46529  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem54  46588  elaa2lem  46661  etransclem9  46671  sge0cl  46809  sge0repnf  46814  sge0split  46837  sge0gtfsumgt  46871  mod2addne  47818  lighneallem1  48068  lighneallem3  48070  gpg3kgrtriexlem5  48563  0nodd  48646  2nodd  48648  1neven  48714