Theorem mtbi 312

Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

Ref	Expression
mtbi.1	|- -. ph
mtbi.2	|- ( ph <-> ps )

Assertion

Ref	Expression
mtbi	|- -. ps

Proof of Theorem mtbi

Step	Hyp	Ref	Expression
1		mtbi.1	. 2 |- -. ph
2		mtbi.2	. . 3 |- ( ph <-> ps )
3	2	biimpri 218	. 2 |- ( ps -> ph )
4	1, 3	mto 188	1 |- -. ps

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

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 197

This theorem is referenced by:  mtbir  313  vprc  4796  vnex  4798  opthwiener  4976  harndom  8469  alephprc  8922  unialeph  8924  ndvdsi  15136  bitsfzo  15157  nprmi  15402  dec2dvds  15767  dec5dvds2  15769  mreexmrid  16303  sinhalfpilem  24215  ppi2i  24895  axlowdimlem13  25834  ex-mod  27306  measvuni  30277  ballotlem2  30550  sgnmulsgp  30612  bnj1224  30872  bnj1541  30926  bnj1311  31092  dfon2lem7  31694  onsucsuccmpi  32442  bj-imn3ani  32572  bj-0nelmpt  33069  bj-pinftynminfty  33114  poimirlem30  33439  clsk1indlem4  38342  alimp-no-surprise  42527