Theorem mtbir 660

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nnexmid  835  nndc  836  fal  1338  ax-9  1511  nonconne  2320  nemtbir  2397  ru  2908  noel  3367  iun0  3869  0iun  3870  br0  3976  vprc  4060  iin0r  4093  nlim0  4316  snnex  4369  onsucelsucexmid  4445  0nelxp  4567  dm0  4753  iprc  4807  co02  5052  0fv  5456  frec0g  6294  nnsucuniel  6391  1nen2  6755  fidcenumlemrk  6842  djulclb  6940  ismkvnex  7029  0nnq  7172  0npr  7291  nqprdisj  7352  0ncn  7639  axpre-ltirr  7690  pnfnre  7807  mnfnre  7808  inelr  8346  xrltnr  9566  fzo0  9945  fzouzdisj  9957  inftonninf  10214  hashinfom  10524  3prm  11809  sqrt2irr  11840  ennnfonelem1  11920  bj-nndcALT  12963  bj-vprc  13094  pwle2  13193  exmidsbthrlem  13217