Theorem mtbir 300

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 205	. 2 |- ( ps <-> ph )
4	1, 3	mtbi 299	1 |- -. ph

Syntax hints:   -. wn 3   <-> wb 187

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 188

This theorem is referenced by:  fal  1444  nonconneOLD  2613  nemtbir  2696  ru  3241  pssirr  3508  indifdir  3672  noel  3708  npss0  3776  iun0  4298  0iun  4299  br0  4413  vprc  4505  iin0  4541  nfnid  4593  opelopabsb  4673  0nelxp  4824  dm0  5010  co02  5311  nlim0  5443  snsn0non  5503  imadif  5619  0fv  5858  snnex  6555  iprc  6686  tfr2b  7069  tz7.44lem1  7078  tz7.48-3  7116  canth2  7678  pwcdadom  8597  canthp1lem2  9029  pwxpndom2  9041  adderpq  9332  mulerpq  9333  0ncn  9508  ax1ne0  9535  pnfnre  9633  mnfnre  9634  inelr  10550  xrltnr  11372  fzouzdisj  11905  lsw0  12660  fprodn0f  13988  eirr  14200  ruc  14238  aleph1re  14240  sqrt2irr  14244  sadc0  14371  1nprm  14572  3prm  14584  prmrec  14809  meet0  16326  join0  16327  odhash  17166  00lsp  18147  zfbas  20853  ustn0  21177  lhop  22910  dvrelog  23524  axlowdimlem13  24926  uvtx01vtx  25162  avril1  25842  helloworld  25844  topnfbey  25848  vsfval  26196  dmadjrnb  27501  xrge00  28399  esumrnmpt2  28841  measvuni  28988  sibf0  29119  ballotlem4  29283  signswch  29402  bnj521  29497  3pm3.2ni  30297  elpotr  30378  dfon2lem7  30386  poseq  30442  nosgnn0  30496  sltsolem1  30506  linedegen  30859  mont  31018  subsym1  31036  limsucncmpi  31054  bj-ru1  31449  bj-0nel1  31457  bj-pinftynrr  31571  bj-minftynrr  31575  bj-pinftynminfty  31576  finxp0  31690  poimirlem30  31877  diophren  35568  stoweidlem44  37788  fourierdlem62  37915  aisbnaxb  38312  dandysum2p2e4  38400  nnsum4primeseven  38708  nnsum4primesevenALTV  38709  0nodd  39401  2nodd  39403  1neven  39523  2zrngnring  39543  ex-gt  40041  alsi-no-surprise  40128