Theorem mtbir 628

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  fal  1291  ax-9  1464  nonconne  2257  nemtbir  2334  ru  2814  noel  3255  iun0  3734  0iun  3735  vprc  3909  iin0r  3943  nlim0  4149  snnex  4199  onsucelsucexmid  4273  0nelxp  4390  dm0  4567  iprc  4618  co02  4854  0fv  5229  frec0g  6006  1nen2  6347  0nnq  6554  0npr  6673  nqprdisj  6734  0ncn  7000  axpre-ltirr  7048  pnfnre  7160  mnfnre  7161  inelr  7684  xrltnr  8855  fzo0  9177  fzouzdisj  9189  3prm  10510  sqrt2irr  10541  nnexmid  10570  nndc  10571  bj-vprc  10687