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

Theorem mtbir 292
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 195 . 2  |-  ( ps  <->  ph )
41, 3mtbi 291 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178
This theorem is referenced by:  fal  1332  nonconne  2614  nemtbir  2698  ru  3166  pssirr  3433  indifdir  3582  noel  3617  npss0  3690  iun0  4171  0iun  4172  vprc  4370  iin0  4402  nfnid  4422  opelopabsb  4494  nlim0  4668  snsn0non  4729  snnex  4742  0nelxp  4935  dm0  5112  iprc  5163  co02  5412  imadif  5557  fv01  5792  tfr2b  6686  tz7.44lem1  6692  tz7.48-3  6730  0we1  6779  canth2  7289  pwcdadom  8127  brdom3  8437  canthwe  8557  canthp1lem2  8559  pwxpndom2  8571  adderpq  8864  mulerpq  8865  0ncn  9039  ax1ne0  9066  pnfnre  9158  mnfnre  9159  inelr  10021  xrltnr  10751  fzouzdisj  11200  eirr  12835  ruc  12873  aleph1re  12875  sqr2irr  12879  sadc0  12997  1nprm  13115  3prm  13127  prmrec  13321  odhash  15239  00lsp  16088  zfbas  17959  ustn0  18281  lhop  19931  dvrelog  20559  uvtx01vtx  21532  avril1  21788  helloworld  21790  vsfval  22145  dmadjrnb  23440  xrge00  24239  measvuni  24599  sibf0  24680  ballotlem4  24787  3pm3.2ni  25198  elpotr  25439  dfon2lem7  25447  poseq  25559  nosgnn0  25644  sltsolem1  25654  axlowdimlem13  25924  linedegen  26108  mont  26190  subsym1  26208  limsucncmpi  26226  diophren  26912  stoweidlem44  27807  aisbnaxb  27893  dandysum2p2e4  27957  ex-gt  28569  bnj521  29202
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 179
  Copyright terms: Public domain W3C validator