MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbir 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  1328  nonconne  2574  nemtbir  2655  ru  3120  pssirr  3407  indifdir  3557  noel  3592  npss0  3626  iun0  4107  0iun  4108  vprc  4301  iin0  4333  nfnid  4353  opelopabsb  4425  nlim0  4599  snsn0non  4659  snnex  4672  0nelxp  4865  dm0  5042  iprc  5093  co02  5342  imadif  5487  fv01  5722  tfr2b  6616  tz7.44lem1  6622  tz7.48-3  6660  0we1  6709  canth2  7219  pwcdadom  8052  brdom3  8362  canthwe  8482  canthp1lem2  8484  pwxpndom2  8496  adderpq  8789  mulerpq  8790  0ncn  8964  ax1ne0  8991  pnfnre  9083  mnfnre  9084  inelr  9946  xrltnr  10676  fzouzdisj  11124  eirr  12759  ruc  12797  aleph1re  12799  sqr2irr  12803  sadc0  12921  1nprm  13039  3prm  13051  prmrec  13245  odhash  15163  00lsp  16012  zfbas  17881  ustn0  18203  lhop  19853  dvrelog  20481  uvtx01vtx  21454  avril1  21710  helloworld  21712  vsfval  22067  dmadjrnb  23362  xrge00  24161  measvuni  24521  sibf0  24602  ballotlem4  24709  3pm3.2ni  25120  elpotr  25351  dfon2lem7  25359  poseq  25467  nosgnn0  25526  sltsolem1  25536  axlowdimlem13  25797  linedegen  25981  mont  26063  subsym1  26081  limsucncmpi  26099  diophren  26764  stoweidlem44  27660  aisbnaxb  27746  dandysum2p2e4  27810  ex-gt  28185  bnj521  28810
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