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  43019  oddfl  43237  dstregt0  43241  xrlttri5d  43243  divlt0gt0d  43246  supxrgere  43293  supxrgelem  43297  supxrge  43298  suplesup  43299  nepnfltpnf  43302  nemnftgtmnft  43304  infrpge  43311  absimnre  43438  iccdifprioo  43476  climfveq  43632  climfveqf  43643  stoweidlem34  43997  stirlinglem5  44041  dirker2re  44055  dirkerdenne0  44056  dirkertrigeq  44064  dirkercncflem2  44067  dirkercncflem4  44069  fourierdlem54  44123  elaa2lem  44196  etransclem9  44206  sge0cl  44344  sge0repnf  44349  sge0split  44372  sge0gtfsumgt  44406  tworepnotupword  44843  lighneallem1  45515  lighneallem3  45517  0nodd  45822  2nodd  45824  1neven  45948
  Copyright terms: Public domain W3C validator