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

Theorem mtbir 290
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 193 . 2  |-  ( ps  <->  ph )
41, 3mtbi 289 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176
This theorem is referenced by:  fal  1313  nonconne  2453  nemtbir  2534  ru  2990  pssirr  3276  indifdir  3425  noel  3459  npss0  3493  iun0  3958  0iun  3959  vprc  4152  iin0  4184  nfnid  4204  opelopabsb  4275  nlim0  4450  snsn0non  4511  snnex  4524  0nelxp  4717  dm0  4892  iprc  4943  co02  5186  imadif  5327  fv01  5559  tfr2b  6412  tz7.44lem1  6418  tz7.48-3  6456  0we1  6505  canth2  7014  pwcdadom  7842  brdom3  8153  canthwe  8273  canthp1lem2  8275  pwxpndom2  8287  adderpq  8580  mulerpq  8581  0ncn  8755  ax1ne0  8782  pnfnre  8874  mnfnre  8875  inelr  9736  xrltnr  10462  fzouzdisj  10902  eirr  12483  ruc  12521  aleph1re  12523  sqr2irr  12527  sadc0  12645  1nprm  12763  3prm  12775  prmrec  12969  odhash  14885  00lsp  15738  zfbas  17591  lhop  19363  dvrelog  19984  avril1  20836  helloworld  20838  vsfval  21191  dmadjrnb  22486  xrge00  23311  measvuni  23542  3pm3.2ni  24064  elpotr  24137  dfon2lem7  24145  poseq  24253  nosgnn0  24312  sltsolem1  24322  funpartfv  24483  axlowdimlem13  24582  linedegen  24766  mont  24848  subsym1  24866  limsucncmpi  24884  inpc  25277  diophren  26896  compneOLD  27643  stoweidlem44  27793  dandysum2p2e4  27943  uvtx01vtx  28164  ex-gt  28198  bnj521  28765
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 177
  Copyright terms: Public domain W3C validator