MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbir Structured version   Unicode version

Theorem mtbir 291
Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.)
Hypotheses
Ref Expression
mtbir.1  |-  -.  ps
mtbir.2  |-  ( ph  <->  ps )
Assertion
Ref Expression
mtbir  |-  -.  ph

Proof of Theorem mtbir
StepHypRef Expression
1 mtbir.1 . 2  |-  -.  ps
2 mtbir.2 . . 3  |-  ( ph  <->  ps )
32bicomi 194 . 2  |-  ( ps  <->  ph )
41, 3mtbi 290 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177
This theorem is referenced by:  fal  1331  nonconne  2605  nemtbir  2686  ru  3152  pssirr  3439  indifdir  3589  noel  3624  npss0  3658  iun0  4139  0iun  4140  vprc  4333  iin0  4365  nfnid  4385  opelopabsb  4457  nlim0  4631  snsn0non  4692  snnex  4705  0nelxp  4898  dm0  5075  iprc  5126  co02  5375  imadif  5520  fv01  5755  tfr2b  6649  tz7.44lem1  6655  tz7.48-3  6693  0we1  6742  canth2  7252  pwcdadom  8086  brdom3  8396  canthwe  8516  canthp1lem2  8518  pwxpndom2  8530  adderpq  8823  mulerpq  8824  0ncn  8998  ax1ne0  9025  pnfnre  9117  mnfnre  9118  inelr  9980  xrltnr  10710  fzouzdisj  11159  eirr  12794  ruc  12832  aleph1re  12834  sqr2irr  12838  sadc0  12956  1nprm  13074  3prm  13086  prmrec  13280  odhash  15198  00lsp  16047  zfbas  17918  ustn0  18240  lhop  19890  dvrelog  20518  uvtx01vtx  21491  avril1  21747  helloworld  21749  vsfval  22104  dmadjrnb  23399  xrge00  24198  measvuni  24558  sibf0  24639  ballotlem4  24746  3pm3.2ni  25157  elpotr  25396  dfon2lem7  25404  poseq  25513  nosgnn0  25578  sltsolem1  25588  axlowdimlem13  25858  linedegen  26042  mont  26124  subsym1  26142  limsucncmpi  26160  diophren  26828  stoweidlem44  27724  aisbnaxb  27810  dandysum2p2e4  27874  ex-gt  28372  bnj521  29005
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator