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 247	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtod 197	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  neleqtrd  2856  eueq3  3708  efrirr  5658  efrn2lp  5659  epne3  7760  wfrlem10OLD  8318  dif1enlem  9156  dif1enlemOLD  9157  ordtypelem9  9521  cantnfp1lem3  9675  cantnflem1b  9681  cantnflem1  9684  cnfcom3lem  9698  cflim2  10258  fin23lem30  10337  isf32lem5  10352  axdc3lem4  10448  axpownd  10596  pwfseqlem3  10655  grur1  10815  genpnnp  11000  xrlttri  13118  expneg  14035  bcval5  14278  seqcoll  14425  seqcoll2  14426  hashge2el2dif  14441  fsumss  15671  fprodss  15892  oddsumodd  16333  rpdvds  16597  pcmpt  16825  prmreclem2  16850  prmreclem5  16853  prmlem0  17039  sylow1lem3  19468  sylow2blem3  19490  efgredlema  19608  gsum2d2lem  19841  simpgnideld  19969  lindsind2  21374  1stccnp  22966  kqdisj  23236  alexsubALTlem4  23554  xrhmeo  24462  minveclem3b  24945  ovolgelb  24997  volsup  25073  volsup2  25122  itg1val2  25201  itg2seq  25260  itg2cn  25281  limcnlp  25395  itgsubstlem  25565  ply1termlem  25717  radcnvlt1  25930  fsumharmonic  26516  ftalem3  26579  chpub  26723  lgsqr  26854  lgseisenlem1  26878  lgsquadlem3  26885  2sqlem8a  26928  2sqlem8  26929  2sqblem  26934  nosupbnd1lem2  27212  nosupbnd2  27219  noinfbnd1lem2  27227  noinfbnd2  27234  axtgupdim2  27722  tgdim01  27758  lnoppnhpg  28015  axcontlem2  28223  minvecolem5  30134  divnumden2  32024  qsnzr  32574  mxidlirred  32588  esum2d  33091  oddpwdc  33353  eulerpartlemsv2  33357  eulerpartlemv  33363  eulerpartlemgh  33377  signslema  33573  erdszelem7  34188  erdszelem8  34189  wsuclem  34797  knoppndvlem10  35397  knoppndvlem13  35400  nlpineqsn  36289  lindsdom  36482  ftc1anclem5  36565  cntotbnd  36664  lshpdisj  37857  lcv1  37911  atlatmstc  38189  hlatcon2  38323  4noncolr3  38324  3atlem6  38359  lplnnleat  38413  lplnexllnN  38435  lvolnleat  38454  4atlem11  38480  dalem1  38530  dalemswapyzps  38561  dalemrotps  38562  2llnma1  38658  dalawlem15  38756  4atexlemcnd  38943  ltrnel  39010  cdleme15c  39147  cdleme0nex  39161  cdleme20m  39194  cdleme43bN  39361  cdleme43dN  39363  cdlemeg46nlpq  39388  cdlemg12  39521  dihmeetcN  40173  dihjatc1  40182  dihjatcclem1  40289  lclkrlem2a  40378  lcfrlem20  40433  mapdh6aN  40606  mapdh8ab  40648  hdmap1l6a  40680  aks4d1p8d1  40949  dffltz  41376  flt4lem5a  41394  flt4lem5b  41395  flt4lem5c  41396  flt4lem5d  41397  flt4lem5e  41398  irrapxlem1  41560  elpell14qr2  41600  elpell1qr2  41610  wepwsolem  41784  fnwe2lem2  41793  brneqtrd  43765  oddfl  43987  dstregt0  43991  xrlttri5d  43993  divlt0gt0d  43996  supxrgere  44043  supxrgelem  44047  supxrge  44048  suplesup  44049  nepnfltpnf  44052  nemnftgtmnft  44054  infrpge  44061  absimnre  44187  iccdifprioo  44229  climfveq  44385  climfveqf  44396  stoweidlem34  44750  stirlinglem5  44794  dirker2re  44808  dirkerdenne0  44809  dirkertrigeq  44817  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem54  44876  elaa2lem  44949  etransclem9  44959  sge0cl  45097  sge0repnf  45102  sge0split  45125  sge0gtfsumgt  45159  tworepnotupword  45600  lighneallem1  46273  lighneallem3  46275  0nodd  46580  2nodd  46582  1neven  46830