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

Theorem mtbid 327
 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 251 . 2 (𝜑 → (𝜒𝜓))
41, 3mtod 201 1 (𝜑 → ¬ 𝜒)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  neleqtrd  2937  eueq3  3688  efrirr  5524  efrn2lp  5525  epne3  7486  wfrlem10  7956  ordtypelem9  8983  cantnfp1lem3  9136  cantnflem1b  9142  cantnflem1  9145  cnfcom3lem  9159  cflim2  9679  fin23lem30  9758  isf32lem5  9773  axdc3lem4  9869  axpownd  10017  pwfseqlem3  10076  grur1  10236  genpnnp  10421  xrlttri  12527  expneg  13440  bcval5  13681  seqcoll  13825  seqcoll2  13826  hashge2el2dif  13841  fsumss  15080  fprodss  15300  oddsumodd  15737  rpdvds  16000  pcmpt  16224  prmreclem2  16249  prmreclem5  16252  prmlem0  16437  sylow1lem3  18723  sylow2blem3  18745  efgredlema  18864  gsum2d2lem  19091  simpgnideld  19219  lindsind2  20958  1stccnp  22065  kqdisj  22335  alexsubALTlem4  22653  xrhmeo  23549  minveclem3b  24030  ovolgelb  24082  volsup  24158  volsup2  24207  itg1val2  24286  itg2seq  24344  itg2cn  24365  limcnlp  24479  itgsubstlem  24649  ply1termlem  24798  radcnvlt1  25011  fsumharmonic  25595  ftalem3  25658  chpub  25802  lgsqr  25933  lgseisenlem1  25957  lgsquadlem3  25964  2sqlem8a  26007  2sqlem8  26008  2sqblem  26013  axtgupdim2  26263  tgdim01  26299  lnoppnhpg  26556  axcontlem2  26757  minvecolem5  28662  divnumden2  30540  esum2d  31379  oddpwdc  31639  eulerpartlemsv2  31643  eulerpartlemv  31649  eulerpartlemgh  31663  signslema  31859  erdszelem7  32471  erdszelem8  32472  wsuclem  33139  nosupbnd1lem2  33236  nosupbnd2  33243  knoppndvlem10  33887  knoppndvlem13  33890  nlpineqsn  34739  lindsdom  34963  ftc1anclem5  35046  cntotbnd  35146  lshpdisj  36195  lcv1  36249  atlatmstc  36527  hlatcon2  36660  4noncolr3  36661  3atlem6  36696  lplnnleat  36750  lplnexllnN  36772  lvolnleat  36791  4atlem11  36817  dalem1  36867  dalemswapyzps  36898  dalemrotps  36899  2llnma1  36995  dalawlem15  37093  4atexlemcnd  37280  ltrnel  37347  cdleme15c  37484  cdleme0nex  37498  cdleme20m  37531  cdleme43bN  37698  cdleme43dN  37700  cdlemeg46nlpq  37725  cdlemg12  37858  dihmeetcN  38510  dihjatc1  38519  dihjatcclem1  38626  lclkrlem2a  38715  lcfrlem20  38770  mapdh6aN  38943  mapdh8ab  38985  hdmap1l6a  39017  dffltz  39471  irrapxlem1  39619  elpell14qr2  39659  elpell1qr2  39669  wepwsolem  39842  fnwe2lem2  39851  brneqtrd  41572  oddfl  41774  dstregt0  41778  xrlttri5d  41780  divlt0gt0d  41783  supxrgere  41831  supxrgelem  41835  supxrge  41836  suplesup  41837  nepnfltpnf  41840  nemnftgtmnft  41842  infrpge  41849  absimnre  41982  iccdifprioo  42019  climfveq  42177  climfveqf  42188  stoweidlem34  42542  stirlinglem5  42586  dirker2re  42600  dirkerdenne0  42601  dirkertrigeq  42609  dirkercncflem2  42612  dirkercncflem4  42614  fourierdlem54  42668  elaa2lem  42741  etransclem9  42751  sge0cl  42886  sge0repnf  42891  sge0split  42914  sge0gtfsumgt  42948  lighneallem1  43989  lighneallem3  43991  0nodd  44296  2nodd  44298  1neven  44422
 Copyright terms: Public domain W3C validator