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  2853  eueq3  3665  efrirr  5599  efrn2lp  5600  epne3  7712  dif1enlem  9075  ordtypelem9  9418  cantnfp1lem3  9576  cantnflem1b  9582  cantnflem1  9585  cnfcom3lem  9599  cflim2  10160  fin23lem30  10239  isf32lem5  10254  axdc3lem4  10350  axpownd  10498  pwfseqlem3  10557  grur1  10717  genpnnp  10902  xrlttri  13044  expneg  13982  bcval5  14231  seqcoll  14377  seqcoll2  14378  hashge2el2dif  14393  fsumss  15638  fprodss  15861  oddsumodd  16307  rpdvds  16577  pcmpt  16810  prmreclem2  16835  prmreclem5  16838  prmlem0  17023  sylow1lem3  19518  sylow2blem3  19540  efgredlema  19658  gsum2d2lem  19891  simpgnideld  20019  lindsind2  21762  1stccnp  23383  kqdisj  23653  alexsubALTlem4  23971  xrhmeo  24877  minveclem3b  25361  ovolgelb  25414  volsup  25490  volsup2  25539  itg1val2  25618  itg2seq  25676  itg2cn  25697  limcnlp  25812  itgsubstlem  25988  ply1termlem  26141  radcnvlt1  26360  fsumharmonic  26955  ftalem3  27018  chpub  27164  lgsqr  27295  lgseisenlem1  27319  lgsquadlem3  27326  2sqlem8a  27369  2sqlem8  27370  2sqblem  27375  nosupbnd1lem2  27654  nosupbnd2  27661  noinfbnd1lem2  27669  noinfbnd2  27676  axtgupdim2  28455  tgdim01  28491  lnoppnhpg  28748  axcontlem2  28950  minvecolem5  30868  divnumden2  32805  qsnzr  33427  mxidlirred  33444  rprmndvdsr1  33496  resssra  33606  extdgfialglem1  33712  esum2d  34113  oddpwdc  34374  eulerpartlemsv2  34378  eulerpartlemv  34384  eulerpartlemgh  34398  signslema  34582  erdszelem7  35248  erdszelem8  35249  wsuclem  35874  knoppndvlem10  36572  knoppndvlem13  36575  nlpineqsn  37459  lindsdom  37660  ftc1anclem5  37743  cntotbnd  37842  lshpdisj  39092  lcv1  39146  atlatmstc  39424  hlatcon2  39557  4noncolr3  39558  3atlem6  39593  lplnnleat  39647  lplnexllnN  39669  lvolnleat  39688  4atlem11  39714  dalem1  39764  dalemswapyzps  39795  dalemrotps  39796  2llnma1  39892  dalawlem15  39990  4atexlemcnd  40177  ltrnel  40244  cdleme15c  40381  cdleme0nex  40395  cdleme20m  40428  cdleme43bN  40595  cdleme43dN  40597  cdlemeg46nlpq  40622  cdlemg12  40755  dihmeetcN  41407  dihjatc1  41416  dihjatcclem1  41523  lclkrlem2a  41612  lcfrlem20  41667  mapdh6aN  41840  mapdh8ab  41882  hdmap1l6a  41914  aks4d1p8d1  42183  mulltgt0d  42581  mullt0b2d  42583  sn-mullt0d  42584  fimgmcyc  42633  dffltz  42733  flt4lem5a  42751  flt4lem5b  42752  flt4lem5c  42753  flt4lem5d  42754  flt4lem5e  42755  irrapxlem1  42920  elpell14qr2  42960  elpell1qr2  42970  wepwsolem  43140  fnwe2lem2  43149  brneqtrd  45178  oddfl  45384  dstregt0  45388  xrlttri5d  45390  divlt0gt0d  45392  supxrgere  45437  supxrgelem  45441  supxrge  45442  suplesup  45443  nepnfltpnf  45446  nemnftgtmnft  45448  infrpge  45455  absimnre  45579  iccdifprioo  45621  climfveq  45772  climfveqf  45783  stoweidlem34  46137  stirlinglem5  46181  dirker2re  46195  dirkerdenne0  46196  dirkertrigeq  46204  dirkercncflem2  46207  dirkercncflem4  46209  fourierdlem54  46263  elaa2lem  46336  etransclem9  46346  sge0cl  46484  sge0repnf  46489  sge0split  46512  sge0gtfsumgt  46546  mod2addne  47469  lighneallem1  47710  lighneallem3  47712  gpg3kgrtriexlem5  48192  0nodd  48275  2nodd  48277  1neven  48343