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  2466  nemtbir  2547  ru  3003  pssirr  3289  indifdir  3438  noel  3472  npss0  3506  iun0  3974  0iun  3975  vprc  4168  iin0  4200  nfnid  4220  opelopabsb  4291  nlim0  4466  snsn0non  4527  snnex  4540  0nelxp  4733  dm0  4908  iprc  4959  co02  5202  imadif  5343  fv01  5575  tfr2b  6428  tz7.44lem1  6434  tz7.48-3  6472  0we1  6521  canth2  7030  pwcdadom  7858  brdom3  8169  canthwe  8289  canthp1lem2  8291  pwxpndom2  8303  adderpq  8596  mulerpq  8597  0ncn  8771  ax1ne0  8798  pnfnre  8890  mnfnre  8891  inelr  9752  xrltnr  10478  fzouzdisj  10918  eirr  12499  ruc  12537  aleph1re  12539  sqr2irr  12543  sadc0  12661  1nprm  12779  3prm  12791  prmrec  12985  odhash  14901  00lsp  15754  zfbas  17607  lhop  19379  dvrelog  20000  avril1  20852  helloworld  20854  vsfval  21207  dmadjrnb  22502  xrge00  23326  measvuni  23557  3pm3.2ni  24079  elpotr  24208  dfon2lem7  24216  poseq  24324  nosgnn0  24383  sltsolem1  24393  axlowdimlem13  24654  linedegen  24838  mont  24920  subsym1  24938  limsucncmpi  24956  inpc  25380  diophren  26999  compneOLD  27746  stoweidlem44  27896  dandysum2p2e4  28046  uvtx01vtx  28305  ex-gt  28452  bnj521  29081
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