Theorem mtbir 297

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 296	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  1405  nonconneOLD  2663  nemtbir  2782  ru  3323  pssirr  3590  indifdir  3751  noel  3787  npss0  3853  iun0  4371  0iun  4372  br0  4485  vprc  4575  iin0  4611  nfnid  4666  opelopabsb  4746  nlim0  4925  snsn0non  4985  0nelxp  5016  dm0  5205  co02  5504  imadif  5645  0fv  5881  snnex  6579  iprc  6708  tfr2b  7057  tz7.44lem1  7063  tz7.48-3  7101  canth2  7663  pwcdadom  8587  canthp1lem2  9020  pwxpndom2  9032  adderpq  9323  mulerpq  9324  0ncn  9499  ax1ne0  9526  pnfnre  9624  mnfnre  9625  inelr  10521  xrltnr  11333  fzouzdisj  11838  lsw0  12574  eirr  14020  ruc  14060  aleph1re  14062  sqrt2irr  14066  sadc0  14188  1nprm  14306  3prm  14318  prmrec  14524  meet0  15966  join0  15967  odhash  16793  00lsp  17822  zfbas  20563  ustn0  20889  lhop  22583  dvrelog  23186  axlowdimlem13  24459  uvtx01vtx  24694  avril1  25373  helloworld  25375  vsfval  25726  dmadjrnb  27023  xrge00  27908  esumrnmpt2  28297  measvuni  28422  sibf0  28540  ballotlem4  28701  signswch  28782  3pm3.2ni  29331  elpotr  29453  dfon2lem7  29461  poseq  29573  nosgnn0  29658  sltsolem1  29668  linedegen  30021  mont  30102  subsym1  30120  limsucncmpi  30138  diophren  30986  fprodn0f  31833  stoweidlem44  32065  fourierdlem62  32190  aisbnaxb  32345  dandysum2p2e4  32409  0nodd  32870  2nodd  32872  1neven  32992  2zrngnring  33012  ex-gt  33512  alsi-no-surprise  33599  bnj521  34193  bj-ru1  34902  bj-0nel1  34910  bj-pinftynrr  35025  bj-minftynrr  35029  bj-pinftynminfty  35030