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  2860  eueq3  3719  efrirr  5668  efrn2lp  5669  epne3  7791  wfrlem10OLD  8356  dif1enlem  9194  dif1enlemOLD  9195  ordtypelem9  9563  cantnfp1lem3  9717  cantnflem1b  9723  cantnflem1  9726  cnfcom3lem  9740  cflim2  10300  fin23lem30  10379  isf32lem5  10394  axdc3lem4  10490  axpownd  10638  pwfseqlem3  10697  grur1  10857  genpnnp  11042  xrlttri  13177  expneg  14106  bcval5  14353  seqcoll  14499  seqcoll2  14500  hashge2el2dif  14515  fsumss  15757  fprodss  15980  oddsumodd  16423  rpdvds  16693  pcmpt  16925  prmreclem2  16950  prmreclem5  16953  prmlem0  17139  sylow1lem3  19632  sylow2blem3  19654  efgredlema  19772  gsum2d2lem  20005  simpgnideld  20133  lindsind2  21856  1stccnp  23485  kqdisj  23755  alexsubALTlem4  24073  xrhmeo  24990  minveclem3b  25475  ovolgelb  25528  volsup  25604  volsup2  25653  itg1val2  25732  itg2seq  25791  itg2cn  25812  limcnlp  25927  itgsubstlem  26103  ply1termlem  26256  radcnvlt1  26475  fsumharmonic  27069  ftalem3  27132  chpub  27278  lgsqr  27409  lgseisenlem1  27433  lgsquadlem3  27440  2sqlem8a  27483  2sqlem8  27484  2sqblem  27489  nosupbnd1lem2  27768  nosupbnd2  27775  noinfbnd1lem2  27783  noinfbnd2  27790  axtgupdim2  28493  tgdim01  28529  lnoppnhpg  28786  axcontlem2  28994  minvecolem5  30909  divnumden2  32821  qsnzr  33462  mxidlirred  33479  rprmndvdsr1  33531  resssra  33616  esum2d  34073  oddpwdc  34335  eulerpartlemsv2  34339  eulerpartlemv  34345  eulerpartlemgh  34359  signslema  34555  erdszelem7  35181  erdszelem8  35182  wsuclem  35806  knoppndvlem10  36503  knoppndvlem13  36506  nlpineqsn  37390  lindsdom  37600  ftc1anclem5  37683  cntotbnd  37782  lshpdisj  38968  lcv1  39022  atlatmstc  39300  hlatcon2  39434  4noncolr3  39435  3atlem6  39470  lplnnleat  39524  lplnexllnN  39546  lvolnleat  39565  4atlem11  39591  dalem1  39641  dalemswapyzps  39672  dalemrotps  39673  2llnma1  39769  dalawlem15  39867  4atexlemcnd  40054  ltrnel  40121  cdleme15c  40258  cdleme0nex  40272  cdleme20m  40305  cdleme43bN  40472  cdleme43dN  40474  cdlemeg46nlpq  40499  cdlemg12  40632  dihmeetcN  41284  dihjatc1  41293  dihjatcclem1  41400  lclkrlem2a  41489  lcfrlem20  41544  mapdh6aN  41717  mapdh8ab  41759  hdmap1l6a  41791  aks4d1p8d1  42065  fimgmcyc  42520  dffltz  42620  flt4lem5a  42638  flt4lem5b  42639  flt4lem5c  42640  flt4lem5d  42641  flt4lem5e  42642  irrapxlem1  42809  elpell14qr2  42849  elpell1qr2  42859  wepwsolem  43030  fnwe2lem2  43039  brneqtrd  45015  oddfl  45227  dstregt0  45231  xrlttri5d  45233  divlt0gt0d  45236  supxrgere  45282  supxrgelem  45286  supxrge  45287  suplesup  45288  nepnfltpnf  45291  nemnftgtmnft  45293  infrpge  45300  absimnre  45426  iccdifprioo  45468  climfveq  45624  climfveqf  45635  stoweidlem34  45989  stirlinglem5  46033  dirker2re  46047  dirkerdenne0  46048  dirkertrigeq  46056  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem54  46115  elaa2lem  46188  etransclem9  46198  sge0cl  46336  sge0repnf  46341  sge0split  46364  sge0gtfsumgt  46398  tworepnotupword  46839  lighneallem1  47529  lighneallem3  47531  0nodd  48013  2nodd  48015  1neven  48081