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

Step	Hyp	Ref	Expression
1		mtbir.1	. 2 |- -. ps
2		mtbir.2	. . 3 |- ( ph <-> ps )
3	2	bicomi 202	. 2 |- ( ps <-> ph )
4	1, 3	mtbi 298	1 |- -. ph

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  1371  nonconne  2613  nemtbir  2698  ru  3182  pssirr  3453  indifdir  3603  noel  3638  npss0  3714  iun0  4223  0iun  4224  br0  4335  sbcbr123  4340  vprc  4427  iin0  4463  nfnid  4518  opelopabsb  4597  nlim0  4773  snsn0non  4833  0nelxp  4863  dm0  5049  co02  5348  imadif  5490  0fv  5720  snnex  6381  iprc  6512  tfr2b  6851  tz7.44lem1  6857  tz7.48-3  6895  0we1  6942  canth2  7460  pwcdadom  8381  brdom3  8691  canthwe  8814  canthp1lem2  8816  pwxpndom2  8828  adderpq  9121  mulerpq  9122  0ncn  9296  ax1ne0  9323  pnfnre  9421  mnfnre  9422  inelr  10308  xrltnr  11097  fzouzdisj  11581  eirr  13483  ruc  13521  aleph1re  13523  sqr2irr  13527  sadc0  13646  1nprm  13764  3prm  13776  prmrec  13979  meet0  15303  join0  15304  odhash  16066  00lsp  17040  zfbas  19369  ustn0  19695  lhop  21388  dvrelog  22025  axlowdimlem13  23119  uvtx01vtx  23319  avril1  23575  helloworld  23577  vsfval  23932  dmadjrnb  25229  xrge00  26064  measvuni  26548  sibf0  26634  ballotlem4  26795  signswch  26876  3pm3.2ni  27282  elpotr  27507  dfon2lem7  27515  poseq  27627  nosgnn0  27712  sltsolem1  27722  linedegen  28087  mont  28169  subsym1  28187  limsucncmpi  28205  diophren  29061  stoweidlem44  29748  aisbnaxb  29834  dandysum2p2e4  29898  ex-gt  30887  alsi-no-surprise  30970  bnj521  31545  bj-0nel1  32142  bj-pinftynrr  32240  bj-minftynrr  32244  bj-pinftynminfty  32245