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  2610  nemtbir  2694  ru  3162  pssirr  3449  indifdir  3599  noel  3634  npss0  3668  iun0  4149  0iun  4150  vprc  4343  iin0  4375  nfnid  4395  opelopabsb  4467  nlim0  4641  snsn0non  4702  snnex  4715  0nelxp  4908  dm0  5085  iprc  5136  co02  5385  imadif  5530  fv01  5765  tfr2b  6659  tz7.44lem1  6665  tz7.48-3  6703  0we1  6752  canth2  7262  pwcdadom  8098  brdom3  8408  canthwe  8528  canthp1lem2  8530  pwxpndom2  8542  adderpq  8835  mulerpq  8836  0ncn  9010  ax1ne0  9037  pnfnre  9129  mnfnre  9130  inelr  9992  xrltnr  10722  fzouzdisj  11171  eirr  12806  ruc  12844  aleph1re  12846  sqr2irr  12850  sadc0  12968  1nprm  13086  3prm  13098  prmrec  13292  odhash  15210  00lsp  16059  zfbas  17930  ustn0  18252  lhop  19902  dvrelog  20530  uvtx01vtx  21503  avril1  21759  helloworld  21761  vsfval  22116  dmadjrnb  23411  xrge00  24210  measvuni  24570  sibf0  24651  ballotlem4  24758  3pm3.2ni  25169  elpotr  25410  dfon2lem7  25418  poseq  25530  nosgnn0  25615  sltsolem1  25625  axlowdimlem13  25895  linedegen  26079  mont  26161  subsym1  26179  limsucncmpi  26197  diophren  26876  stoweidlem44  27771  aisbnaxb  27857  dandysum2p2e4  27921  ex-gt  28533  bnj521  29166
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 179
  Copyright terms: Public domain W3C validator