MPE Home 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  2859  eueq3  3629  efrirr  5537  efrn2lp  5538  epne3  7563  wfrlem10  8069  dif1enlem  8843  ordtypelem9  9147  cantnfp1lem3  9300  cantnflem1b  9306  cantnflem1  9309  cnfcom3lem  9323  cflim2  9882  fin23lem30  9961  isf32lem5  9976  axdc3lem4  10072  axpownd  10220  pwfseqlem3  10279  grur1  10439  genpnnp  10624  xrlttri  12734  expneg  13648  bcval5  13889  seqcoll  14035  seqcoll2  14036  hashge2el2dif  14051  fsumss  15294  fprodss  15515  oddsumodd  15956  rpdvds  16222  pcmpt  16450  prmreclem2  16475  prmreclem5  16478  prmlem0  16664  sylow1lem3  18994  sylow2blem3  19016  efgredlema  19135  gsum2d2lem  19363  simpgnideld  19491  lindsind2  20786  1stccnp  22364  kqdisj  22634  alexsubALTlem4  22952  xrhmeo  23848  minveclem3b  24330  ovolgelb  24382  volsup  24458  volsup2  24507  itg1val2  24586  itg2seq  24645  itg2cn  24666  limcnlp  24780  itgsubstlem  24950  ply1termlem  25102  radcnvlt1  25315  fsumharmonic  25899  ftalem3  25962  chpub  26106  lgsqr  26237  lgseisenlem1  26261  lgsquadlem3  26268  2sqlem8a  26311  2sqlem8  26312  2sqblem  26317  axtgupdim2  26567  tgdim01  26603  lnoppnhpg  26860  axcontlem2  27061  minvecolem5  28967  divnumden2  30857  esum2d  31778  oddpwdc  32038  eulerpartlemsv2  32042  eulerpartlemv  32048  eulerpartlemgh  32062  signslema  32258  erdszelem7  32877  erdszelem8  32878  wsuclem  33561  nosupbnd1lem2  33654  nosupbnd2  33661  noinfbnd1lem2  33669  noinfbnd2  33676  knoppndvlem10  34443  knoppndvlem13  34446  nlpineqsn  35321  lindsdom  35513  ftc1anclem5  35596  cntotbnd  35696  lshpdisj  36743  lcv1  36797  atlatmstc  37075  hlatcon2  37208  4noncolr3  37209  3atlem6  37244  lplnnleat  37298  lplnexllnN  37320  lvolnleat  37339  4atlem11  37365  dalem1  37415  dalemswapyzps  37446  dalemrotps  37447  2llnma1  37543  dalawlem15  37641  4atexlemcnd  37828  ltrnel  37895  cdleme15c  38032  cdleme0nex  38046  cdleme20m  38079  cdleme43bN  38246  cdleme43dN  38248  cdlemeg46nlpq  38273  cdlemg12  38406  dihmeetcN  39058  dihjatc1  39067  dihjatcclem1  39174  lclkrlem2a  39263  lcfrlem20  39318  mapdh6aN  39491  mapdh8ab  39533  hdmap1l6a  39565  dffltz  40182  flt4lem5a  40200  flt4lem5b  40201  flt4lem5c  40202  flt4lem5d  40203  flt4lem5e  40204  irrapxlem1  40355  elpell14qr2  40395  elpell1qr2  40405  wepwsolem  40578  fnwe2lem2  40587  brneqtrd  42307  oddfl  42496  dstregt0  42500  xrlttri5d  42502  divlt0gt0d  42505  supxrgere  42553  supxrgelem  42557  supxrge  42558  suplesup  42559  nepnfltpnf  42562  nemnftgtmnft  42564  infrpge  42571  absimnre  42700  iccdifprioo  42737  climfveq  42893  climfveqf  42904  stoweidlem34  43258  stirlinglem5  43302  dirker2re  43316  dirkerdenne0  43317  dirkertrigeq  43325  dirkercncflem2  43328  dirkercncflem4  43330  fourierdlem54  43384  elaa2lem  43457  etransclem9  43467  sge0cl  43602  sge0repnf  43607  sge0split  43630  sge0gtfsumgt  43664  lighneallem1  44738  lighneallem3  44740  0nodd  45045  2nodd  45047  1neven  45171
  Copyright terms: Public domain W3C validator