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  1377  nonconne  2657  nemtbir  2777  ru  3287  pssirr  3559  indifdir  3709  noel  3744  npss0  3820  iun0  4329  0iun  4330  br0  4441  sbcbr123  4446  vprc  4533  iin0  4569  nfnid  4624  opelopabsb  4702  nlim0  4880  snsn0non  4940  0nelxp  4970  dm0  5156  co02  5454  imadif  5596  0fv  5827  snnex  6487  iprc  6618  tfr2b  6960  tz7.44lem1  6966  tz7.48-3  7004  0we1  7051  canth2  7569  pwcdadom  8491  brdom3  8801  canthwe  8924  canthp1lem2  8926  pwxpndom2  8938  adderpq  9231  mulerpq  9232  0ncn  9406  ax1ne0  9433  pnfnre  9531  mnfnre  9532  inelr  10418  xrltnr  11207  fzouzdisj  11697  eirr  13600  ruc  13638  aleph1re  13640  sqr2irr  13644  sadc0  13763  1nprm  13881  3prm  13893  prmrec  14096  meet0  15421  join0  15422  odhash  16189  00lsp  17180  zfbas  19596  ustn0  19922  lhop  21616  dvrelog  22210  axlowdimlem13  23347  uvtx01vtx  23547  avril1  23803  helloworld  23805  vsfval  24160  dmadjrnb  25457  xrge00  26287  measvuni  26768  sibf0  26859  ballotlem4  27020  signswch  27101  3pm3.2ni  27508  elpotr  27733  dfon2lem7  27741  poseq  27853  nosgnn0  27938  sltsolem1  27948  linedegen  28313  mont  28394  subsym1  28412  limsucncmpi  28430  diophren  29295  stoweidlem44  29982  aisbnaxb  30068  dandysum2p2e4  30132  ex-gt  31372  alsi-no-surprise  31461  bnj521  32041  bj-ru1  32749  bj-0nel1  32757  bj-pinftynrr  32864  bj-minftynrr  32868  bj-pinftynminfty  32869