Theorem mtbir 673

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 672	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  852  nndc  853  fal  1380  ax-9  1554  nonconne  2388  nemtbir  2465  ru  2997  noel  3464  iun0  3984  0iun  3985  br0  4092  vprc  4176  iin0r  4213  nlim0  4441  snnex  4495  onsucelsucexmid  4578  0nelxp  4703  dm0  4892  iprc  4947  co02  5196  0fv  5612  frec0g  6483  nnsucuniel  6581  1nen2  6958  fidcenumlemrk  7056  djulclb  7157  ismkvnex  7257  pw1ne3  7342  sucpw1nel3  7345  3nsssucpw1  7348  0nnq  7477  0npr  7596  nqprdisj  7657  0ncn  7944  axpre-ltirr  7995  pnfnre  8114  mnfnre  8115  inelr  8657  xrltnr  9901  fzo0  10292  fzouzdisj  10304  inftonninf  10587  hashinfom  10923  lsw0  11041  3prm  12450  sqrt2irr  12484  ennnfonelem1  12778  bj-nndcALT  15694  bj-vprc  15832  pwle2  15935  exmidsbthrlem  15961