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  2859  eueq3  3670  efrirr  5605  efrn2lp  5606  epne3  7720  dif1enlem  9088  ordtypelem9  9435  cantnfp1lem3  9593  cantnflem1b  9599  cantnflem1  9602  cnfcom3lem  9616  cflim2  10177  fin23lem30  10256  isf32lem5  10271  axdc3lem4  10367  axpownd  10516  pwfseqlem3  10575  grur1  10735  genpnnp  10920  xrlttri  13057  expneg  13996  bcval5  14245  seqcoll  14391  seqcoll2  14392  hashge2el2dif  14407  fsumss  15652  fprodss  15875  oddsumodd  16321  rpdvds  16591  pcmpt  16824  prmreclem2  16849  prmreclem5  16852  prmlem0  17037  sylow1lem3  19533  sylow2blem3  19555  efgredlema  19673  gsum2d2lem  19906  simpgnideld  20034  lindsind2  21778  1stccnp  23410  kqdisj  23680  alexsubALTlem4  23998  xrhmeo  24904  minveclem3b  25388  ovolgelb  25441  volsup  25517  volsup2  25566  itg1val2  25645  itg2seq  25703  itg2cn  25724  limcnlp  25839  itgsubstlem  26015  ply1termlem  26168  radcnvlt1  26387  fsumharmonic  26982  ftalem3  27045  chpub  27191  lgsqr  27322  lgseisenlem1  27346  lgsquadlem3  27353  2sqlem8a  27396  2sqlem8  27397  2sqblem  27402  nosupbnd1lem2  27681  nosupbnd2  27688  noinfbnd1lem2  27696  noinfbnd2  27703  axtgupdim2  28547  tgdim01  28583  lnoppnhpg  28840  axcontlem2  29042  minvecolem5  30960  divnumden2  32898  qsnzr  33538  mxidlirred  33555  rprmndvdsr1  33607  esplyind  33733  resssra  33745  extdgfialglem1  33851  esum2d  34252  oddpwdc  34513  eulerpartlemsv2  34517  eulerpartlemv  34523  eulerpartlemgh  34537  signslema  34721  erdszelem7  35393  erdszelem8  35394  wsuclem  36019  knoppndvlem10  36723  knoppndvlem13  36726  nlpineqsn  37615  lindsdom  37817  ftc1anclem5  37900  cntotbnd  37999  lshpdisj  39315  lcv1  39369  atlatmstc  39647  hlatcon2  39780  4noncolr3  39781  3atlem6  39816  lplnnleat  39870  lplnexllnN  39892  lvolnleat  39911  4atlem11  39937  dalem1  39987  dalemswapyzps  40018  dalemrotps  40019  2llnma1  40115  dalawlem15  40213  4atexlemcnd  40400  ltrnel  40467  cdleme15c  40604  cdleme0nex  40618  cdleme20m  40651  cdleme43bN  40818  cdleme43dN  40820  cdlemeg46nlpq  40845  cdlemg12  40978  dihmeetcN  41630  dihjatc1  41639  dihjatcclem1  41746  lclkrlem2a  41835  lcfrlem20  41890  mapdh6aN  42063  mapdh8ab  42105  hdmap1l6a  42137  aks4d1p8d1  42406  mulltgt0d  42804  mullt0b2d  42806  sn-mullt0d  42807  fimgmcyc  42856  dffltz  42944  flt4lem5a  42962  flt4lem5b  42963  flt4lem5c  42964  flt4lem5d  42965  flt4lem5e  42966  irrapxlem1  43131  elpell14qr2  43171  elpell1qr2  43181  wepwsolem  43351  fnwe2lem2  43360  brneqtrd  45388  oddfl  45593  dstregt0  45597  xrlttri5d  45599  divlt0gt0d  45601  supxrgere  45645  supxrgelem  45649  supxrge  45650  suplesup  45651  nepnfltpnf  45654  nemnftgtmnft  45656  infrpge  45663  absimnre  45787  iccdifprioo  45829  climfveq  45980  climfveqf  45991  stoweidlem34  46345  stirlinglem5  46389  dirker2re  46403  dirkerdenne0  46404  dirkertrigeq  46412  dirkercncflem2  46415  dirkercncflem4  46417  fourierdlem54  46471  elaa2lem  46544  etransclem9  46554  sge0cl  46692  sge0repnf  46697  sge0split  46720  sge0gtfsumgt  46754  mod2addne  47677  lighneallem1  47918  lighneallem3  47920  gpg3kgrtriexlem5  48400  0nodd  48483  2nodd  48485  1neven  48551