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

Theorem mtbid 312
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 236 . 2 (𝜑 → (𝜒𝜓))
41, 3mtod 187 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194
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 195
This theorem is referenced by:  sylnib  316  neleqtrd  2708  eueq3  3347  efrirr  5008  efrn2lp  5009  epne3  6849  wfrlem10  7288  ordtypelem9  8291  cantnfp1lem3  8437  cantnflem1b  8443  cantnflem1  8446  cnfcom3lem  8460  cflim2  8945  fin23lem30  9024  isf32lem5  9039  axdc3lem4  9135  axpownd  9279  pwfseqlem3  9338  grur1  9498  genpnnp  9683  xrlttri  11809  expneg  12687  bcval5  12924  seqcoll  13059  seqcoll2  13060  hashge2el2dif  13069  fsumss  14251  fprodss  14465  oddsumodd  14899  rpdvds  15160  pcmpt  15382  prmreclem2  15407  prmreclem5  15410  prmlem0  15598  sylow1lem3  17786  sylow2blem3  17808  efgredlema  17924  gsum2d2lem  18143  lindsind2  19924  1stccnp  21022  kqdisj  21292  alexsubALTlem4  21611  xrhmeo  22500  minveclem3b  22951  ovolgelb  22999  volsup  23075  volsup2  23123  itg1val2  23201  itg2seq  23259  itg2cn  23280  limcnlp  23392  itgsubstlem  23559  ply1termlem  23707  radcnvlt1  23920  fsumharmonic  24482  ftalem3  24545  chpub  24689  lgsqr  24820  lgseisenlem1  24844  lgsquadlem3  24851  2sqlem8a  24894  2sqlem8  24895  2sqblem  24900  tgdim01  25146  lnoppnhpg  25401  acopyeu  25470  axcontlem2  25590  usgraedgrnv  25699  minvecolem5  26914  divnumden2  28744  esum2d  29275  oddpwdc  29536  eulerpartlemsv2  29540  eulerpartlemv  29546  eulerpartlemgh  29560  signslema  29758  erdszelem7  30226  erdszelem8  30227  wsuclem  30810  wsuclemOLD  30811  knoppndvlem10  31475  knoppndvlem13  31478  lindsdom  32356  ftc1anclem5  32442  cntotbnd  32548  lshpdisj  33075  lcv1  33129  atlatmstc  33407  hlatcon2  33539  4noncolr3  33540  3atlem6  33575  lplnnleat  33629  lplnexllnN  33651  lvolnleat  33670  4atlem11  33696  dalem1  33746  dalemswapyzps  33777  dalemrotps  33778  2llnma1  33874  dalawlem15  33972  4atexlemcnd  34159  ltrnel  34226  cdleme15c  34364  cdleme0nex  34378  cdleme20yOLD  34391  cdleme20m  34412  cdleme43bN  34579  cdleme43dN  34581  cdlemeg46nlpq  34606  cdlemg12  34739  dihmeetcN  35392  dihjatc1  35401  dihjatcclem1  35508  lclkrlem2a  35597  lcfrlem20  35652  mapdh6aN  35825  mapdh8ab  35867  hdmap1l6a  35900  irrapxlem1  36187  elpell14qr2  36227  elpell1qr2  36237  wepwsolem  36413  fnwe2lem2  36422  brneqtrd  38057  oddfl  38213  dstregt0  38217  xrlttri5d  38219  divlt0gt0d  38222  supxrgere  38273  supxrgelem  38277  supxrge  38278  suplesup  38279  nepnfltpnf  38282  nemnftgtmnft  38284  infrpge  38291  iccdifprioo  38372  climfveq  38519  stoweidlem34  38710  stirlinglem5  38754  dirker2re  38768  dirkerdenne0  38769  dirkertrigeq  38777  dirkercncflem2  38780  dirkercncflem4  38782  fourierdlem54  38836  elaa2lem  38909  etransclem9  38919  sge0cl  39057  sge0repnf  39062  sge0split  39085  sge0gtfsumgt  39119  lighneallem1  39844  lighneallem3  39846  0nodd  41581  2nodd  41583  1neven  41703
  Copyright terms: Public domain W3C validator