Theorem mtbir 671

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  850  nndc  851  fal  1360  ax-9  1531  nonconne  2359  nemtbir  2436  ru  2962  noel  3427  iun0  3944  0iun  3945  br0  4052  vprc  4136  iin0r  4170  nlim0  4395  snnex  4449  onsucelsucexmid  4530  0nelxp  4655  dm0  4842  iprc  4896  co02  5143  0fv  5551  frec0g  6398  nnsucuniel  6496  1nen2  6861  fidcenumlemrk  6953  djulclb  7054  ismkvnex  7153  pw1ne3  7229  sucpw1nel3  7232  3nsssucpw1  7235  0nnq  7363  0npr  7482  nqprdisj  7543  0ncn  7830  axpre-ltirr  7881  pnfnre  7999  mnfnre  8000  inelr  8541  xrltnr  9779  fzo0  10168  fzouzdisj  10180  inftonninf  10441  hashinfom  10758  3prm  12128  sqrt2irr  12162  ennnfonelem1  12408  bj-nndcALT  14513  bj-vprc  14651  pwle2  14751  exmidsbthrlem  14773