Theorem mtbi 289

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 197	. 2 |- ( ps -> ph )
4	1, 3	mto 167	1 |- -. ps

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

This theorem is referenced by:  mtbir  290  mtp-xor  1525  vprc  4152  vnex  4154  opthwiener  4268  harndom  7278  alephprc  7726  unialeph  7728  ndvdsi  12609  bitsfzo  12626  nprmi  12773  dec2dvds  13078  dec5dvds2  13080  mreexmrid  13545  sinhalfpilem  19834  ppi2i  20407  measvuni  23542  dfon2lem7  24145  sltval2  24310  axlowdimlem13  24582  onsucsuccmpi  24882  jm2.23  27089  compneOLD  27643  bnj1224  28834  bnj1541  28888  bnj1311  29054

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177