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  2850  eueq3  3682  efrirr  5618  efrn2lp  5619  epne3  7749  dif1enlem  9120  dif1enlemOLD  9121  ordtypelem9  9479  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1  9642  cnfcom3lem  9656  cflim2  10216  fin23lem30  10295  isf32lem5  10310  axdc3lem4  10406  axpownd  10554  pwfseqlem3  10613  grur1  10773  genpnnp  10958  xrlttri  13099  expneg  14034  bcval5  14283  seqcoll  14429  seqcoll2  14430  hashge2el2dif  14445  fsumss  15691  fprodss  15914  oddsumodd  16360  rpdvds  16630  pcmpt  16863  prmreclem2  16888  prmreclem5  16891  prmlem0  17076  sylow1lem3  19530  sylow2blem3  19552  efgredlema  19670  gsum2d2lem  19903  simpgnideld  20031  lindsind2  21728  1stccnp  23349  kqdisj  23619  alexsubALTlem4  23937  xrhmeo  24844  minveclem3b  25328  ovolgelb  25381  volsup  25457  volsup2  25506  itg1val2  25585  itg2seq  25643  itg2cn  25664  limcnlp  25779  itgsubstlem  25955  ply1termlem  26108  radcnvlt1  26327  fsumharmonic  26922  ftalem3  26985  chpub  27131  lgsqr  27262  lgseisenlem1  27286  lgsquadlem3  27293  2sqlem8a  27336  2sqlem8  27337  2sqblem  27342  nosupbnd1lem2  27621  nosupbnd2  27628  noinfbnd1lem2  27636  noinfbnd2  27643  axtgupdim2  28398  tgdim01  28434  lnoppnhpg  28691  axcontlem2  28892  minvecolem5  30810  divnumden2  32740  qsnzr  33426  mxidlirred  33443  rprmndvdsr1  33495  resssra  33583  esum2d  34083  oddpwdc  34345  eulerpartlemsv2  34349  eulerpartlemv  34355  eulerpartlemgh  34369  signslema  34553  erdszelem7  35184  erdszelem8  35185  wsuclem  35813  knoppndvlem10  36509  knoppndvlem13  36512  nlpineqsn  37396  lindsdom  37608  ftc1anclem5  37691  cntotbnd  37790  lshpdisj  38980  lcv1  39034  atlatmstc  39312  hlatcon2  39446  4noncolr3  39447  3atlem6  39482  lplnnleat  39536  lplnexllnN  39558  lvolnleat  39577  4atlem11  39603  dalem1  39653  dalemswapyzps  39684  dalemrotps  39685  2llnma1  39781  dalawlem15  39879  4atexlemcnd  40066  ltrnel  40133  cdleme15c  40270  cdleme0nex  40284  cdleme20m  40317  cdleme43bN  40484  cdleme43dN  40486  cdlemeg46nlpq  40511  cdlemg12  40644  dihmeetcN  41296  dihjatc1  41305  dihjatcclem1  41412  lclkrlem2a  41501  lcfrlem20  41556  mapdh6aN  41729  mapdh8ab  41771  hdmap1l6a  41803  aks4d1p8d1  42072  mulltgt0d  42470  mullt0b2d  42472  sn-mullt0d  42473  fimgmcyc  42522  dffltz  42622  flt4lem5a  42640  flt4lem5b  42641  flt4lem5c  42642  flt4lem5d  42643  flt4lem5e  42644  irrapxlem1  42810  elpell14qr2  42850  elpell1qr2  42860  wepwsolem  43031  fnwe2lem2  43040  brneqtrd  45070  oddfl  45276  dstregt0  45280  xrlttri5d  45282  divlt0gt0d  45284  supxrgere  45329  supxrgelem  45333  supxrge  45334  suplesup  45335  nepnfltpnf  45338  nemnftgtmnft  45340  infrpge  45347  absimnre  45472  iccdifprioo  45514  climfveq  45667  climfveqf  45678  stoweidlem34  46032  stirlinglem5  46076  dirker2re  46090  dirkerdenne0  46091  dirkertrigeq  46099  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem54  46158  elaa2lem  46231  etransclem9  46241  sge0cl  46379  sge0repnf  46384  sge0split  46407  sge0gtfsumgt  46441  tworepnotupword  46884  mod2addne  47365  lighneallem1  47606  lighneallem3  47608  gpg3kgrtriexlem5  48078  0nodd  48158  2nodd  48160  1neven  48226