Theorem mtbir 290

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 193	. 2 |- (ps <-> ph)
4	1, 3	mtbi 289	1 |- -. ph

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

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

This theorem is referenced by:  fal  1322  nonconne  2523  nemtbir  2604  ru  3045  pssirr  3369  indifdir  3511  necompl  3544  noel  3554  npss0  3589  iun0  4022  0iun  4023  0nel1c  4159  0nelsuc  4400  nndisjeq  4429  addcnul1  4452  eqtfinrelk  4486  nulnnn  4556  0cnelphi  4597  dm0  4918  cnv0  5031  co02  5092  co01  5093  nfunv  5138  imadif  5171  fv01  5354  1p1e2c  6155  2p1e3c  6156  fnfreclem2  6318