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

Theorem mtbir 323
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 223 . 2 (𝜓𝜑)
41, 3mtbi 322 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205
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 206
This theorem is referenced by:  3pm3.2ni  1489  fal  1556  eqneltri  2857  nemtbir  3041  ru  3739  pssirr  4061  indifdirOLD  4246  noel  4291  noelOLD  4292  iun0  5023  0iun  5024  br0  5155  vprc  5273  iin0  5318  nfnid  5331  opelopabsb  5488  0nelopab  5525  0nelxp  5668  0xp  5731  nrelv  5757  dm0  5877  cnv0  6094  co02  6213  nlim0  6377  snsn0non  6443  imadif  6586  0fv  6887  poxp2  8076  poseq  8091  tz7.44lem1  8352  nlim1  8436  nlim2  8437  sdom0  9053  canth2  9075  snnen2o  9182  1sdom2  9185  canthp1lem2  10590  pwxpndom2  10602  adderpq  10893  mulerpq  10894  0ncn  11070  ax1ne0  11097  inelr  12144  xrltnr  13041  fzouzdisj  13609  lsw0  14454  eirr  16088  ruc  16126  aleph1re  16128  sqrt2irr  16132  n2dvds1  16251  n2dvds3  16254  sadc0  16335  1nprm  16556  join0  18295  meet0  18296  smndex1n0mnd  18723  nsmndex1  18724  smndex2dnrinv  18726  odhash  19357  cnfldfun  20811  zringndrg  20892  zfbas  23250  ustn0  23575  zclmncvs  24515  lhop  25383  dvrelog  25995  nosgnn0  27009  sltsolem1  27026  addsid1  27279  axlowdimlem13  27906  ntrl2v2e  29105  konigsberglem4  29202  avril1  29410  helloworld  29412  topnfbey  29416  vsfval  29578  dmadjrnb  30851  xrge00  31880  esumrnmpt2  32670  measvuni  32816  sibf0  32937  ballotlem4  33101  signswch  33176  satf0n0  33975  fmlaomn0  33987  gonan0  33989  goaln0  33990  fmla0disjsuc  33995  elpotr  34359  dfon2lem7  34367  muls01  34412  muls02  34413  mulsid1  34414  mulsid2  34415  linedegen  34731  nmotru  34883  limsucncmpi  34920  bj-ru1  35417  bj-0nel1  35427  bj-inftyexpitaudisj  35679  bj-pinftynminfty  35701  finxp0  35865  poimirlem30  36111  coss0  36944  epnsymrel  37027  diophren  41139  notbicom  43388  rexanuz2nf  43735  stoweidlem44  44292  fourierdlem62  44416  salexct2  44587  aisbnaxb  45153  dandysum2p2e4  45240  iota0ndef  45280  aiota0ndef  45336  257prm  45760  fmtno4nprmfac193  45773  139prmALT  45795  31prm  45796  127prm  45798  nnsum4primeseven  45999  nnsum4primesevenALTV  46000  0nodd  46111  2nodd  46113  1neven  46237  2zrngnring  46257  ex-gt  47180  alsi-no-surprise  47250
  Copyright terms: Public domain W3C validator