MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbir 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
mtbir.2
Assertion
Ref Expression
mtbir

Proof of Theorem mtbir
StepHypRef Expression
1 mtbir.1 . 2
2 mtbir.2 . . 3
32bicomi 202 . 2
41, 3mtbi 298 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184
This theorem is referenced by:  fal  1402  nonconneOLD  2666  nemtbir  2785  ru  3326  pssirr  3603  indifdir  3753  noel  3788  npss0  3865  iun0  4386  0iun  4387  br0  4498  vprc  4590  iin0  4626  nfnid  4681  opelopabsb  4762  nlim0  4941  snsn0non  5001  0nelxp  5032  dm0  5221  co02  5526  imadif  5668  0fv  5904  snnex  6606  iprc  6735  tfr2b  7084  tz7.44lem1  7090  tz7.48-3  7128  canth2  7690  pwcdadom  8617  canthp1lem2  9052  pwxpndom2  9064  adderpq  9355  mulerpq  9356  0ncn  9531  ax1ne0  9558  pnfnre  9656  mnfnre  9657  inelr  10551  xrltnr  11359  fzouzdisj  11861  eirr  13938  ruc  13976  aleph1re  13978  sqrt2irr  13982  sadc0  14104  1nprm  14222  3prm  14234  prmrec  14440  meet0  15767  join0  15768  odhash  16594  00lsp  17627  zfbas  20397  ustn0  20723  lhop  22417  dvrelog  23018  axlowdimlem13  24257  uvtx01vtx  24492  avril1  25171  helloworld  25173  vsfval  25528  dmadjrnb  26825  xrge00  27674  measvuni  28185  sibf0  28276  ballotlem4  28437  signswch  28518  3pm3.2ni  29090  elpotr  29213  dfon2lem7  29221  poseq  29333  nosgnn0  29418  sltsolem1  29428  linedegen  29793  mont  29874  subsym1  29892  limsucncmpi  29910  diophren  30747  fprodn0f  31594  stoweidlem44  31826  fourierdlem62  31951  aisbnaxb  32106  dandysum2p2e4  32170  0nodd  32498  2nodd  32500  1neven  32738  2zrngnring  32758  ex-gt  33122  alsi-no-surprise  33211  bnj521  33792  bj-ru1  34501  bj-0nel1  34509  bj-pinftynrr  34625  bj-minftynrr  34629  bj-pinftynminfty  34630
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
  Copyright terms: Public domain W3C validator