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

Theorem mtbir 299
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 202 . 2  |-  ( ps  <->  ph )
41, 3mtbi 298 1  |-  -.  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184
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 185
This theorem is referenced by:  fal  1386  nonconneOLD  2676  nemtbir  2795  ru  3330  pssirr  3604  indifdir  3754  noel  3789  npss0  3865  iun0  4381  0iun  4382  br0  4493  sbcbr123  4498  vprc  4585  iin0  4621  nfnid  4676  opelopabsb  4757  nlim0  4936  snsn0non  4996  0nelxp  5027  dm0  5216  co02  5521  imadif  5663  0fv  5899  snnex  6590  iprc  6719  tfr2b  7065  tz7.44lem1  7071  tz7.48-3  7109  0we1  7156  canth2  7670  pwcdadom  8596  brdom3  8906  canthwe  9029  canthp1lem2  9031  pwxpndom2  9043  adderpq  9334  mulerpq  9335  0ncn  9510  ax1ne0  9537  pnfnre  9635  mnfnre  9636  inelr  10526  xrltnr  11330  fzouzdisj  11829  eirr  13799  ruc  13837  aleph1re  13839  sqrt2irr  13843  sadc0  13963  1nprm  14081  3prm  14093  prmrec  14299  meet0  15624  join0  15625  odhash  16400  00lsp  17427  zfbas  20160  ustn0  20486  lhop  22180  dvrelog  22774  axlowdimlem13  23961  uvtx01vtx  24196  avril1  24875  helloworld  24877  vsfval  25232  dmadjrnb  26529  xrge00  27364  measvuni  27853  sibf0  27944  ballotlem4  28105  signswch  28186  3pm3.2ni  28593  elpotr  28818  dfon2lem7  28826  poseq  28938  nosgnn0  29023  sltsolem1  29033  linedegen  29398  mont  29479  subsym1  29497  limsucncmpi  29515  diophren  30379  stoweidlem44  31372  fourierdlem62  31497  aisbnaxb  31601  dandysum2p2e4  31665  ex-gt  32221  alsi-no-surprise  32310  bnj521  32890  bj-ru1  33600  bj-0nel1  33608  bj-pinftynrr  33715  bj-minftynrr  33719  bj-pinftynminfty  33720
  Copyright terms: Public domain W3C validator