Theorem mtbid 327

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  neleqtrd  2882  eueq3  3669  efrirr  5628  efrn2lp  5629  epne3  7771  dif1enlem  9154  ordtypelem9  9498  cantnfp1lem3  9659  cantnflem1b  9665  cantnflem1  9668  cnfcom3lem  9682  cflim2  10298  fin23lem30  10377  isf32lem5  10392  axdc3lem4  10488  axpownd  10643  pwfseqlem3  10702  grur1  10862  genpnnp  11047  xrlttri  13223  expneg  14166  bcval5  14415  seqcoll  14562  seqcoll2  14563  hashge2el2dif  14578  fsumss  15844  fprodss  16068  oddsumodd  16513  rpdvds  16783  pcmpt  17017  prmreclem2  17042  prmreclem5  17045  prmlem0  17230  sylow1lem3  19761  sylow2blem3  19783  efgredlema  19901  gsum2d2lem  20134  simpgnideld  20262  qsnzr  21586  lindsind2  22072  lindsdom  22103  1stccnp  23728  kqdisj  23998  alexsubALTlem4  24316  xrhmeo  25214  minveclem3b  25696  ovolgelb  25748  volsup  25824  volsup2  25873  itg1val2  25952  itg2seq  26010  itg2cn  26031  limcnlp  26145  itgsubstlem  26315  ply1termlem  26468  radcnvlt1  26694  fsumharmonic  27288  ftalem3  27351  chpub  27496  lgsqr  27627  lgseisenlem1  27651  lgsquadlem3  27658  2sqlem8a  27701  2sqlem8  27702  2sqblem  27707  nosupbnd1lem2  27985  nosupbnd2  27992  noinfbnd1lem2  28000  noinfbnd2  28007  axtgupdim2  28852  tgdim01  28889  lnoppnhpg  29161  axcontlem2  29462  minvecolem5  31402  divnumden2  33326  mxidlirred  33916  rprmndvdsr1  33975  esplyind  34126  resssra  34138  extdgfialglem1  34243  esum2d  34644  oddpwdc  34906  eulerpartlemsv2  34910  eulerpartlemv  34916  eulerpartlemgh  34930  signslema  35111  erdszelem7  35877  erdszelem8  35878  wsuclem  36503  knoppndvlem10  37303  knoppndvlem13  37306  nlpineqsn  38245  ftc1anclem5  38529  cntotbnd  38644  lshpdisj  39958  lcv1  40012  atlatmstc  40290  hlatcon2  40423  4noncolr3  40424  3atlem6  40459  lplnnleat  40513  lplnexllnN  40535  lvolnleat  40554  4atlem11  40580  dalem1  40630  dalemswapyzps  40661  dalemrotps  40662  2llnma1  40758  dalawlem15  40856  4atexlemcnd  41043  ltrnel  41110  cdleme15c  41247  cdleme0nex  41261  cdleme20m  41294  cdleme43bN  41461  cdleme43dN  41463  cdlemeg46nlpq  41488  cdlemg12  41621  dihmeetcN  42273  dihjatc1  42282  dihjatcclem1  42389  lclkrlem2a  42478  lcfrlem20  42533  mapdh6aN  42706  mapdh8ab  42748  hdmap1l6a  42780  aks4d1p8d1  43048  mulltgt0d  43468  mullt0b2d  43470  sn-mullt0d  43471  fimgmcyc  43514  dffltz  43578  flt4lem5a  43596  flt4lem5b  43597  flt4lem5c  43598  flt4lem5d  43599  flt4lem5e  43600  irrapxlem1  43761  elpell14qr2  43801  elpell1qr2  43811  wepwsolem  43981  fnwe2lem2  43990  brneqtrd  46008  oddfl  46209  dstregt0  46213  xrlttri5d  46215  divlt0gt0d  46217  supxrgere  46261  supxrgelem  46265  supxrge  46266  suplesup  46267  nepnfltpnf  46270  nemnftgtmnft  46272  infrpge  46279  absimnre  46402  iccdifprioo  46444  climfveq  46595  climfveqf  46606  stoweidlem34  46960  stirlinglem5  47004  dirker2re  47018  dirkerdenne0  47019  dirkertrigeq  47027  dirkercncflem2  47030  dirkercncflem4  47032  fourierdlem54  47086  elaa2lem  47159  etransclem9  47169  sge0cl  47307  sge0repnf  47312  sge0split  47335  sge0gtfsumgt  47369  mod2addne  48356  lighneallem1  48606  lighneallem3  48608  gpg3kgrtriexlem5  49101  0nodd  49183  2nodd  49185  1neven  49251  veroquaddetzerod  50902