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  2854  eueq3  3707  efrirr  5657  efrn2lp  5658  epne3  7764  wfrlem10OLD  8324  dif1enlem  9162  dif1enlemOLD  9163  ordtypelem9  9527  cantnfp1lem3  9681  cantnflem1b  9687  cantnflem1  9690  cnfcom3lem  9704  cflim2  10264  fin23lem30  10343  isf32lem5  10358  axdc3lem4  10454  axpownd  10602  pwfseqlem3  10661  grur1  10821  genpnnp  11006  xrlttri  13125  expneg  14042  bcval5  14285  seqcoll  14432  seqcoll2  14433  hashge2el2dif  14448  fsumss  15678  fprodss  15899  oddsumodd  16340  rpdvds  16604  pcmpt  16832  prmreclem2  16857  prmreclem5  16860  prmlem0  17046  sylow1lem3  19516  sylow2blem3  19538  efgredlema  19656  gsum2d2lem  19889  simpgnideld  20017  lindsind2  21684  1stccnp  23286  kqdisj  23556  alexsubALTlem4  23874  xrhmeo  24791  minveclem3b  25276  ovolgelb  25329  volsup  25405  volsup2  25454  itg1val2  25533  itg2seq  25592  itg2cn  25613  limcnlp  25727  itgsubstlem  25903  ply1termlem  26055  radcnvlt1  26269  fsumharmonic  26858  ftalem3  26921  chpub  27067  lgsqr  27198  lgseisenlem1  27222  lgsquadlem3  27229  2sqlem8a  27272  2sqlem8  27273  2sqblem  27278  nosupbnd1lem2  27556  nosupbnd2  27563  noinfbnd1lem2  27571  noinfbnd2  27578  axtgupdim2  28156  tgdim01  28192  lnoppnhpg  28449  axcontlem2  28657  minvecolem5  30568  divnumden2  32458  qsnzr  33015  mxidlirred  33029  resssra  33129  esum2d  33556  oddpwdc  33818  eulerpartlemsv2  33822  eulerpartlemv  33828  eulerpartlemgh  33842  signslema  34038  erdszelem7  34653  erdszelem8  34654  wsuclem  35268  knoppndvlem10  35863  knoppndvlem13  35866  nlpineqsn  36755  lindsdom  36948  ftc1anclem5  37031  cntotbnd  37130  lshpdisj  38323  lcv1  38377  atlatmstc  38655  hlatcon2  38789  4noncolr3  38790  3atlem6  38825  lplnnleat  38879  lplnexllnN  38901  lvolnleat  38920  4atlem11  38946  dalem1  38996  dalemswapyzps  39027  dalemrotps  39028  2llnma1  39124  dalawlem15  39222  4atexlemcnd  39409  ltrnel  39476  cdleme15c  39613  cdleme0nex  39627  cdleme20m  39660  cdleme43bN  39827  cdleme43dN  39829  cdlemeg46nlpq  39854  cdlemg12  39987  dihmeetcN  40639  dihjatc1  40648  dihjatcclem1  40755  lclkrlem2a  40844  lcfrlem20  40899  mapdh6aN  41072  mapdh8ab  41114  hdmap1l6a  41146  aks4d1p8d1  41418  dffltz  41841  flt4lem5a  41859  flt4lem5b  41860  flt4lem5c  41861  flt4lem5d  41862  flt4lem5e  41863  irrapxlem1  42025  elpell14qr2  42065  elpell1qr2  42075  wepwsolem  42249  fnwe2lem2  42258  brneqtrd  44229  oddfl  44448  dstregt0  44452  xrlttri5d  44454  divlt0gt0d  44457  supxrgere  44504  supxrgelem  44508  supxrge  44509  suplesup  44510  nepnfltpnf  44513  nemnftgtmnft  44515  infrpge  44522  absimnre  44648  iccdifprioo  44690  climfveq  44846  climfveqf  44857  stoweidlem34  45211  stirlinglem5  45255  dirker2re  45269  dirkerdenne0  45270  dirkertrigeq  45278  dirkercncflem2  45281  dirkercncflem4  45283  fourierdlem54  45337  elaa2lem  45410  etransclem9  45420  sge0cl  45558  sge0repnf  45563  sge0split  45586  sge0gtfsumgt  45620  tworepnotupword  46061  lighneallem1  46734  lighneallem3  46736  0nodd  47009  2nodd  47011  1neven  47077