Theorem mtbi 291

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

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

This theorem is referenced by:  mtbir  292  mtp-xorOLD  1547  vprc  4344  vnex  4346  opthwiener  4461  harndom  7535  alephprc  7985  unialeph  7987  ndvdsi  12935  bitsfzo  12952  nprmi  13099  dec2dvds  13404  dec5dvds2  13406  mreexmrid  13873  sinhalfpilem  20379  ppi2i  20957  measvuni  24573  ballotlem2  24751  dfon2lem7  25421  sltval2  25616  axlowdimlem13  25898  onsucsuccmpi  26198  jm2.23  27081  bnj1224  29247  bnj1541  29301  bnj1311  29467

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 179