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

Theorem mtbid 313
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 237 . 2 (𝜑 → (𝜒𝜓))
41, 3mtod 188 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195
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 196
This theorem is referenced by:  sylnib  317  neleqtrd  2709  eueq3  3348  efrirr  5019  efrn2lp  5020  epne3  6872  wfrlem10  7311  ordtypelem9  8314  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1  8469  cnfcom3lem  8483  cflim2  8968  fin23lem30  9047  isf32lem5  9062  axdc3lem4  9158  axpownd  9302  pwfseqlem3  9361  grur1  9521  genpnnp  9706  xrlttri  11848  expneg  12730  bcval5  12967  seqcoll  13105  seqcoll2  13106  hashge2el2dif  13117  fsumss  14303  fprodss  14517  oddsumodd  14951  rpdvds  15212  pcmpt  15434  prmreclem2  15459  prmreclem5  15462  prmlem0  15650  sylow1lem3  17838  sylow2blem3  17860  efgredlema  17976  gsum2d2lem  18195  lindsind2  19977  1stccnp  21075  kqdisj  21345  alexsubALTlem4  21664  xrhmeo  22553  minveclem3b  23007  ovolgelb  23055  volsup  23131  volsup2  23179  itg1val2  23257  itg2seq  23315  itg2cn  23336  limcnlp  23448  itgsubstlem  23615  ply1termlem  23763  radcnvlt1  23976  fsumharmonic  24538  ftalem3  24601  chpub  24745  lgsqr  24876  lgseisenlem1  24900  lgsquadlem3  24907  2sqlem8a  24950  2sqlem8  24951  2sqblem  24956  tgdim01  25202  lnoppnhpg  25456  acopyeu  25525  axcontlem2  25645  usgraedgrnv  25906  minvecolem5  27121  divnumden2  28951  esum2d  29482  oddpwdc  29743  eulerpartlemsv2  29747  eulerpartlemv  29753  eulerpartlemgh  29767  signslema  29965  erdszelem7  30433  erdszelem8  30434  wsuclem  31017  wsuclemOLD  31018  knoppndvlem10  31682  knoppndvlem13  31685  lindsdom  32573  ftc1anclem5  32659  cntotbnd  32765  lshpdisj  33292  lcv1  33346  atlatmstc  33624  hlatcon2  33756  4noncolr3  33757  3atlem6  33792  lplnnleat  33846  lplnexllnN  33868  lvolnleat  33887  4atlem11  33913  dalem1  33963  dalemswapyzps  33994  dalemrotps  33995  2llnma1  34091  dalawlem15  34189  4atexlemcnd  34376  ltrnel  34443  cdleme15c  34581  cdleme0nex  34595  cdleme20yOLD  34608  cdleme20m  34629  cdleme43bN  34796  cdleme43dN  34798  cdlemeg46nlpq  34823  cdlemg12  34956  dihmeetcN  35609  dihjatc1  35618  dihjatcclem1  35725  lclkrlem2a  35814  lcfrlem20  35869  mapdh6aN  36042  mapdh8ab  36084  hdmap1l6a  36117  irrapxlem1  36404  elpell14qr2  36444  elpell1qr2  36454  wepwsolem  36630  fnwe2lem2  36639  brneqtrd  38274  oddfl  38430  dstregt0  38434  xrlttri5d  38436  divlt0gt0d  38439  supxrgere  38490  supxrgelem  38494  supxrge  38495  suplesup  38496  nepnfltpnf  38499  nemnftgtmnft  38501  infrpge  38508  iccdifprioo  38589  climfveq  38736  stoweidlem34  38927  stirlinglem5  38971  dirker2re  38985  dirkerdenne0  38986  dirkertrigeq  38994  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem54  39053  elaa2lem  39126  etransclem9  39136  sge0cl  39274  sge0repnf  39279  sge0split  39302  sge0gtfsumgt  39336  lighneallem1  40060  lighneallem3  40062  0nodd  41600  2nodd  41602  1neven  41722
  Copyright terms: Public domain W3C validator