Theorem mtbi 290

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

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

This theorem is referenced by:  mtbir  291  mtp-xorOLD  1543  vprc  4301  vnex  4303  opthwiener  4418  harndom  7488  alephprc  7936  unialeph  7938  ndvdsi  12885  bitsfzo  12902  nprmi  13049  dec2dvds  13354  dec5dvds2  13356  mreexmrid  13823  sinhalfpilem  20327  ppi2i  20905  measvuni  24521  ballotlem2  24699  dfon2lem7  25359  sltval2  25524  axlowdimlem13  25797  onsucsuccmpi  26097  jm2.23  26957  bnj1224  28879  bnj1541  28933  bnj1311  29099

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 178