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

Theorem mtbid 323
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 247 . 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  2859  eueq3  3667  efrirr  5611  efrn2lp  5612  epne3  7697  wfrlem10OLD  8231  dif1enlem  9033  dif1enlemOLD  9034  ordtypelem9  9395  cantnfp1lem3  9549  cantnflem1b  9555  cantnflem1  9558  cnfcom3lem  9572  cflim2  10132  fin23lem30  10211  isf32lem5  10226  axdc3lem4  10322  axpownd  10470  pwfseqlem3  10529  grur1  10689  genpnnp  10874  xrlttri  12986  expneg  13903  bcval5  14145  seqcoll  14290  seqcoll2  14291  hashge2el2dif  14306  fsumss  15544  fprodss  15765  oddsumodd  16206  rpdvds  16470  pcmpt  16698  prmreclem2  16723  prmreclem5  16726  prmlem0  16912  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  27211  tgdim01  27247  lnoppnhpg  27504  axcontlem2  27712  minvecolem5  29621  divnumden2  31508  esum2d  32465  oddpwdc  32727  eulerpartlemsv2  32731  eulerpartlemv  32737  eulerpartlemgh  32751  signslema  32947  erdszelem7  33564  erdszelem8  33565  wsuclem  34204  knoppndvlem10  34879  knoppndvlem13  34882  nlpineqsn  35774  lindsdom  35967  ftc1anclem5  36050  cntotbnd  36150  lshpdisj  37344  lcv1  37398  atlatmstc  37676  hlatcon2  37810  4noncolr3  37811  3atlem6  37846  lplnnleat  37900  lplnexllnN  37922  lvolnleat  37941  4atlem11  37967  dalem1  38017  dalemswapyzps  38048  dalemrotps  38049  2llnma1  38145  dalawlem15  38243  4atexlemcnd  38430  ltrnel  38497  cdleme15c  38634  cdleme0nex  38648  cdleme20m  38681  cdleme43bN  38848  cdleme43dN  38850  cdlemeg46nlpq  38875  cdlemg12  39008  dihmeetcN  39660  dihjatc1  39669  dihjatcclem1  39776  lclkrlem2a  39865  lcfrlem20  39920  mapdh6aN  40093  mapdh8ab  40135  hdmap1l6a  40167  aks4d1p8d1  40436  dffltz  40837  flt4lem5a  40855  flt4lem5b  40856  flt4lem5c  40857  flt4lem5d  40858  flt4lem5e  40859  irrapxlem1  41010  elpell14qr2  41050  elpell1qr2  41060  wepwsolem  41234  fnwe2lem2  41243  brneqtrd  43050  oddfl  43268  dstregt0  43272  xrlttri5d  43274  divlt0gt0d  43277  supxrgere  43324  supxrgelem  43328  supxrge  43329  suplesup  43330  nepnfltpnf  43333  nemnftgtmnft  43335  infrpge  43342  absimnre  43469  iccdifprioo  43507  climfveq  43663  climfveqf  43674  stoweidlem34  44028  stirlinglem5  44072  dirker2re  44086  dirkerdenne0  44087  dirkertrigeq  44095  dirkercncflem2  44098  dirkercncflem4  44100  fourierdlem54  44154  elaa2lem  44227  etransclem9  44237  sge0cl  44375  sge0repnf  44380  sge0split  44403  sge0gtfsumgt  44437  tworepnotupword  44874  lighneallem1  45546  lighneallem3  45548  0nodd  45853  2nodd  45855  1neven  45979
  Copyright terms: Public domain W3C validator