MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbid Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 mtbid.min . 2 (𝜑 → ¬ 𝜓)
2 mtbid.maj . . 3 (𝜑 → (𝜓𝜒))
32biimprd 248 . 2 (𝜑 → (𝜒𝜓))
41, 3mtod 197 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
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  3668  efrirr  5612  efrn2lp  5613  epne3  7698  wfrlem10OLD  8232  dif1enlem  9034  dif1enlemOLD  9035  ordtypelem9  9396  cantnfp1lem3  9550  cantnflem1b  9556  cantnflem1  9559  cnfcom3lem  9573  cflim2  10133  fin23lem30  10212  isf32lem5  10227  axdc3lem4  10323  axpownd  10471  pwfseqlem3  10530  grur1  10690  genpnnp  10875  xrlttri  12987  expneg  13904  bcval5  14146  seqcoll  14291  seqcoll2  14292  hashge2el2dif  14307  fsumss  15545  fprodss  15766  oddsumodd  16207  rpdvds  16471  pcmpt  16699  prmreclem2  16724  prmreclem5  16727  prmlem0  16913  sylow1lem3  19311  sylow2blem3  19333  efgredlema  19451  gsum2d2lem  19679  simpgnideld  19807  lindsind2  21148  1stccnp  22735  kqdisj  23005  alexsubALTlem4  23323  xrhmeo  24231  minveclem3b  24714  ovolgelb  24766  volsup  24842  volsup2  24891  itg1val2  24970  itg2seq  25029  itg2cn  25050  limcnlp  25164  itgsubstlem  25334  ply1termlem  25486  radcnvlt1  25699  fsumharmonic  26283  ftalem3  26346  chpub  26490  lgsqr  26621  lgseisenlem1  26645  lgsquadlem3  26652  2sqlem8a  26695  2sqlem8  26696  2sqblem  26701  nosupbnd1lem2  26979  nosupbnd2  26986  noinfbnd1lem2  26994  noinfbnd2  27001  axtgupdim2  27199  tgdim01  27235  lnoppnhpg  27492  axcontlem2  27700  minvecolem5  29609  divnumden2  31496  esum2d  32453  oddpwdc  32715  eulerpartlemsv2  32719  eulerpartlemv  32725  eulerpartlemgh  32739  signslema  32935  erdszelem7  33552  erdszelem8  33553  wsuclem  34192  knoppndvlem10  34870  knoppndvlem13  34873  nlpineqsn  35765  lindsdom  35958  ftc1anclem5  36041  cntotbnd  36141  lshpdisj  37335  lcv1  37389  atlatmstc  37667  hlatcon2  37801  4noncolr3  37802  3atlem6  37837  lplnnleat  37891  lplnexllnN  37913  lvolnleat  37932  4atlem11  37958  dalem1  38008  dalemswapyzps  38039  dalemrotps  38040  2llnma1  38136  dalawlem15  38234  4atexlemcnd  38421  ltrnel  38488  cdleme15c  38625  cdleme0nex  38639  cdleme20m  38672  cdleme43bN  38839  cdleme43dN  38841  cdlemeg46nlpq  38866  cdlemg12  38999  dihmeetcN  39651  dihjatc1  39660  dihjatcclem1  39767  lclkrlem2a  39856  lcfrlem20  39911  mapdh6aN  40084  mapdh8ab  40126  hdmap1l6a  40158  aks4d1p8d1  40427  dffltz  40806  flt4lem5a  40824  flt4lem5b  40825  flt4lem5c  40826  flt4lem5d  40827  flt4lem5e  40828  irrapxlem1  40979  elpell14qr2  41019  elpell1qr2  41029  wepwsolem  41203  fnwe2lem2  41212  brneqtrd  43020  oddfl  43225  dstregt0  43229  xrlttri5d  43231  divlt0gt0d  43234  supxrgere  43281  supxrgelem  43285  supxrge  43286  suplesup  43287  nepnfltpnf  43290  nemnftgtmnft  43292  infrpge  43299  absimnre  43426  iccdifprioo  43464  climfveq  43620  climfveqf  43631  stoweidlem34  43985  stirlinglem5  44029  dirker2re  44043  dirkerdenne0  44044  dirkertrigeq  44052  dirkercncflem2  44055  dirkercncflem4  44057  fourierdlem54  44111  elaa2lem  44184  etransclem9  44194  sge0cl  44330  sge0repnf  44335  sge0split  44358  sge0gtfsumgt  44392  tworepnotupword  44825  lighneallem1  45497  lighneallem3  45499  0nodd  45804  2nodd  45806  1neven  45930
  Copyright terms: Public domain W3C validator