Theorem mtbid 323

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  2860  eueq3  3641  efrirr  5561  efrn2lp  5562  epne3  7601  wfrlem10OLD  8120  dif1enlem  8905  ordtypelem9  9215  cantnfp1lem3  9368  cantnflem1b  9374  cantnflem1  9377  cnfcom3lem  9391  cflim2  9950  fin23lem30  10029  isf32lem5  10044  axdc3lem4  10140  axpownd  10288  pwfseqlem3  10347  grur1  10507  genpnnp  10692  xrlttri  12802  expneg  13718  bcval5  13960  seqcoll  14106  seqcoll2  14107  hashge2el2dif  14122  fsumss  15365  fprodss  15586  oddsumodd  16027  rpdvds  16293  pcmpt  16521  prmreclem2  16546  prmreclem5  16549  prmlem0  16735  sylow1lem3  19120  sylow2blem3  19142  efgredlema  19261  gsum2d2lem  19489  simpgnideld  19617  lindsind2  20936  1stccnp  22521  kqdisj  22791  alexsubALTlem4  23109  xrhmeo  24015  minveclem3b  24497  ovolgelb  24549  volsup  24625  volsup2  24674  itg1val2  24753  itg2seq  24812  itg2cn  24833  limcnlp  24947  itgsubstlem  25117  ply1termlem  25269  radcnvlt1  25482  fsumharmonic  26066  ftalem3  26129  chpub  26273  lgsqr  26404  lgseisenlem1  26428  lgsquadlem3  26435  2sqlem8a  26478  2sqlem8  26479  2sqblem  26484  axtgupdim2  26736  tgdim01  26772  lnoppnhpg  27029  axcontlem2  27236  minvecolem5  29144  divnumden2  31034  esum2d  31961  oddpwdc  32221  eulerpartlemsv2  32225  eulerpartlemv  32231  eulerpartlemgh  32245  signslema  32441  erdszelem7  33059  erdszelem8  33060  wsuclem  33746  nosupbnd1lem2  33839  nosupbnd2  33846  noinfbnd1lem2  33854  noinfbnd2  33861  knoppndvlem10  34628  knoppndvlem13  34631  nlpineqsn  35506  lindsdom  35698  ftc1anclem5  35781  cntotbnd  35881  lshpdisj  36928  lcv1  36982  atlatmstc  37260  hlatcon2  37393  4noncolr3  37394  3atlem6  37429  lplnnleat  37483  lplnexllnN  37505  lvolnleat  37524  4atlem11  37550  dalem1  37600  dalemswapyzps  37631  dalemrotps  37632  2llnma1  37728  dalawlem15  37826  4atexlemcnd  38013  ltrnel  38080  cdleme15c  38217  cdleme0nex  38231  cdleme20m  38264  cdleme43bN  38431  cdleme43dN  38433  cdlemeg46nlpq  38458  cdlemg12  38591  dihmeetcN  39243  dihjatc1  39252  dihjatcclem1  39359  lclkrlem2a  39448  lcfrlem20  39503  mapdh6aN  39676  mapdh8ab  39718  hdmap1l6a  39750  aks4d1p8d1  40020  dffltz  40387  flt4lem5a  40405  flt4lem5b  40406  flt4lem5c  40407  flt4lem5d  40408  flt4lem5e  40409  irrapxlem1  40560  elpell14qr2  40600  elpell1qr2  40610  wepwsolem  40783  fnwe2lem2  40792  brneqtrd  42515  oddfl  42705  dstregt0  42709  xrlttri5d  42711  divlt0gt0d  42714  supxrgere  42762  supxrgelem  42766  supxrge  42767  suplesup  42768  nepnfltpnf  42771  nemnftgtmnft  42773  infrpge  42780  absimnre  42907  iccdifprioo  42944  climfveq  43100  climfveqf  43111  stoweidlem34  43465  stirlinglem5  43509  dirker2re  43523  dirkerdenne0  43524  dirkertrigeq  43532  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem54  43591  elaa2lem  43664  etransclem9  43674  sge0cl  43809  sge0repnf  43814  sge0split  43837  sge0gtfsumgt  43871  lighneallem1  44945  lighneallem3  44947  0nodd  45252  2nodd  45254  1neven  45378